|
Opened structures |
---|
Value summary |
---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Value detail |
---|
val init
val next
fun stringOfTab_T n
tex
n
fun append_with_lemma tab l s
tab
l
s
fun lemma_fusion s1 s2
s1
s2
fun stringOfCommand tab form tex c
tab
form
tex
c
fun stringOfSequence tab form tex s
tab
form
tex
s
fun stringOfExpression tab form tex e
tab
form
tex
e
fun stringOfExpressionList tab form tex el
tab
form
tex
el
fun stringOfValue tab form tex v
tab
form
tex
v
fun max_width sl
sl
fun make_spc n
n
fun tabulate max
max
sl
fun complete (l1, l2)
l1
l2
fun stringOfTyping form tex p
: bool -> bool -> string list -> ProofAst.program -> string list
form
tex
pr
p
|