index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
hol-light
/
TacticRecording
Mode
Name
Size
-rw-r--r--
INSTRUCTIONS
1273
log
plain
-rw-r--r--
LIMITATIONS
949
log
plain
-rw-r--r--
biolayout.ml
1159
log
plain
-rw-r--r--
dltree.ml
10119
log
plain
-rw-r--r--
dltree.mli
1030
log
plain
-rw-r--r--
ex.dot
359
log
plain
-rw-r--r--
ex2.dot
180
log
plain
-rw-r--r--
ex3.dot
390
log
plain
-rw-r--r--
ex3.png
39644
log
plain
-rw-r--r--
ex3b.dot
791
log
plain
-rw-r--r--
examples1.ml
1159
log
plain
-rw-r--r--
examples1_output.txt
1247
log
plain
-rw-r--r--
examples2.ml
1471
log
plain
-rw-r--r--
examples3.ml
9426
log
plain
-rw-r--r--
examples3_LEMMA1.dot
339
log
plain
-rw-r--r--
examples3_output.txt
1988
log
plain
-rw-r--r--
examples4.ml
421
log
plain
-rw-r--r--
examples5.ml
6877
log
plain
-rw-r--r--
gvexport.ml
1924
log
plain
-rw-r--r--
hiproofs.ml
12703
log
plain
-rw-r--r--
lib.ml
1596
log
plain
-rw-r--r--
main.ml
693
log
plain
-rw-r--r--
mldata.ml
565
log
plain
-rw-r--r--
mlexport.ml
6221
log
plain
-rw-r--r--
printutils.ml
2079
log
plain
-rw-r--r--
promote.ml
14010
log
plain
-rw-r--r--
prooftree.ml
7037
log
plain
-rw-r--r--
tacticrec.ml
12736
log
plain
-rw-r--r--
wrappers.ml
13174
log
plain
-rw-r--r--
xtactics.ml
17800
log
plain
-rw-r--r--
xthm.ml
779
log
plain