ProofTree (nholz)

ProofTree Module

Namespace: HOL
Assembly: nholz.dll

Types

Type	Description
Exp
InfRule
Proof
goal

Functions and values

Function or value	Description
`exp loc` Full Usage: `exp loc` Parameters: loc : `Proof Location` Returns: `Exp`	loc : `Proof Location` Returns: `Exp`
`is_goal exp` Full Usage: `is_goal exp` Parameters: exp : `Exp` Returns: `bool`	exp : `Exp` Returns: `bool`
`linearizeProof tr` Full Usage: `linearizeProof tr` Parameters: tr : `Proof Tree`	tr : `Proof Tree`
`loc_goal loc` Full Usage: `loc_goal loc` Parameters: loc : `Proof Location` Returns: `Exp option`	loc : `Proof Location` Returns: `Exp option`
`loc_term loc` Full Usage: `loc_term loc` Parameters: loc : `Proof Location` Returns: `term option`	loc : `Proof Location` Returns: `term option`
`loc_thm loc` Full Usage: `loc_thm loc` Parameters: loc : `Proof Location` Returns: `thm option`	loc : `Proof Location` Returns: `thm option`
`lower` Full Usage: `lower` Returns: `Proof Location -> Proof Location`	Returns: `Proof Location -> Proof Location`
`printExp e` Full Usage: `printExp e` Parameters: e : `Exp` Returns: `string`	e : `Exp` Returns: `string`
`replace x y s` Full Usage: `replace x y s` Parameters: x : `string` y : `string` s : `string` Returns: `string`	x : `string` y : `string` s : `string` Returns: `string`
`strTolatex s` Full Usage: `strTolatex s` Parameters: s : `string` Returns: `string`	s : `string` Returns: `string`
`substs` Full Usage: `substs` Returns: `(string * string) list`	Returns: `(string * string) list`
`treeToLatex ntabs exp tr` Full Usage: `treeToLatex ntabs exp tr` Parameters: ntabs : `int` exp : `Exp` tr : `Proof Tree` Returns: `string`	ntabs : `int` exp : `Exp` tr : `Proof Tree` Returns: `string`
`view loc` Full Usage: `view loc` Parameters: loc : `Proof Location` Returns: `Proof Location`	loc : `Proof Location` Returns: `Proof Location`