InfRule Type

Namespace: HOL
Assembly: nholz.dll
Parent Module: ProofTree
Base Type: obj

Union cases

Union case Description

InstTmLstThmFn (term * term) list -> thm -> thm

Full Usage: InstTmLstThmFn (term * term) list -> thm -> thm

Parameters:
Item : (term * term) list -> thm -> thm

InstTyLstThmFn (hol_type * hol_type) list -> thm -> thm

Full Usage: InstTyLstThmFn (hol_type * hol_type) list -> thm -> thm

Parameters:
Item : (hol_type * hol_type) list -> thm -> thm

NullFun

Full Usage: NullFun

ThmFn thm -> thm

Full Usage: ThmFn thm -> thm

Parameters:
Item : thm -> thm

ThmLstFn thm list -> thm

Full Usage: ThmLstFn thm list -> thm

Parameters:
Item : thm list -> thm

ThmThmFn thm -> thm -> thm

Full Usage: ThmThmFn thm -> thm -> thm

Parameters:
Item : thm -> thm -> thm

ThmThmThmFn thm -> thm -> thm -> thm

Full Usage: ThmThmThmFn thm -> thm -> thm -> thm

Parameters:
Item : thm -> thm -> thm -> thm

ThmTmFn thm -> term -> thm

Full Usage: ThmTmFn thm -> term -> thm

Parameters:
Item : thm -> term -> thm

TmFn term -> thm

Full Usage: TmFn term -> thm

Parameters:
Item : term -> thm

TmLstThmFn term list -> thm -> thm

Full Usage: TmLstThmFn term list -> thm -> thm

Parameters:
Item : term list -> thm -> thm

TmThm2ThmFn term * thm -> thm -> thm

Full Usage: TmThm2ThmFn term * thm -> thm -> thm

Parameters:
Item : term * thm -> thm -> thm

TmThmFn term -> thm -> thm

Full Usage: TmThmFn term -> thm -> thm

Parameters:
Item : term -> thm -> thm

TmThmThmFn term -> thm -> thm -> thm

Full Usage: TmThmThmFn term -> thm -> thm -> thm

Parameters:
Item : term -> thm -> thm -> thm

TmTmThmFn term * term -> thm -> thm

Full Usage: TmTmThmFn term * term -> thm -> thm

Parameters:
Item : term * term -> thm -> thm