forked from HOL-Theorem-Prover/HOL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
.gitignore
131 lines (114 loc) · 2.25 KB
/
.gitignore
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
*Script
*Theory.sig
*Theory.sml
*Theory.dat
*.uo
*.ui
*.o
.hollogs
.HOLMK
*.lex.sml
*.grm.sig
*.grm.sml
*.grm-sig.sml
*.grm.desc
*.exe
.DS_Store
# LaTeX guff
*.aux
*.log
*.toc
*.dvi
*.out
*.idx
*.ilg
*.ind
*.bbl
*.blg
*.tde
*.tid
*.tix
*.hix
*.fdb_latexmk
*.synctex.gz
#Generated Verilog from Iyoda/Gordon hw compilation
*.vl
config-override
tools-poly/poly-includes.ML
.kernelidstr
*~
build-log
svn-update
developers/generateBuildSummary
developers/comparelogs
developers/docfiles/*.txt
tools*/Holmake/Systeml.sml
tools/Holmake/Lexer.sml
tools/Holmake/Parser.sig
tools/Holmake/Parser.sml
sigobj/*
tools/hol-mode.el
tools/quote-filter/filter.sml
tools/quote-filter/quote-filter
tools/quote-filter/selftest
tools/vim/filetype.vim
tools/vim/hol-config.sml
tools/vim/hol.vim
tools/vim/vimhol.sml
tools-poly/build-logs
tools/build-stamp
tools/lastbuildoptions
tools/build-logs
help/Docfiles/*.txt
help/Docfiles/HTML/*
help/HOLindex.html
help/HOL.Help
help/src-sml/htmlsigs
help/src-sml/index.tex
help/src-sml/index.txt
help/theorygraph/*.html
help/theorygraph/theories.dot
help/theorygraph/theories.imap
help/theorygraph/theories.svg
help/theorygraph/theories.pdf
src/bool/SharingTables.*
src/emit/ML/*.sml
src/emit/ML/*.sig
src/emit/Caml/*.ml
src/emit/Caml/*.mli
src/quotient/Manual/quotient.pdf
src/quotient/src/*.html
src/quotient/src/*.lst
src/HolSat/sat_solvers/zc2hs/*.h
src/HolSat/sat_solvers/zc2hs/zc2hs
src/HolSat/sat_solvers/minisat/minisat
src/HolSat/sat_solvers/minisat/depend.mak
src/num/arith/Manual/arith.pdf
src/num/arith/Manual/arith.ps
src/num/termination/numheap
src/num/termination/numheap.o
src/parse/base_lexer.sml
src/quotient/examples/*/*.html
src/quotient/examples/*/*.lst
src/quotient/examples/*.html
src/quotient/examples/*.lst
src/res_quan/help/thms/
src/string/help
src/TeX/holindex-demo.pdf
src/TeX/holindex-demo.ps
*.art
Manual/*/*.pdf
Manual/*/*.ps
Manual/Reference/entries.tex
Manual/Translations/*/*/*.pdf
examples/dev/*.vl
examples/machine-code/lisp/*.s
examples/machine-code/just-in-time/*.s
examples/muddy/muddyC/Makefile
examples/muddy/muddyC/buddy/src/libbdd.a
examples/muddy/muddyC/muddy.so
examples/theorem-prover/lisp-runtime/bin/*.s
examples/computability/lambda/computability-heap
local-hol-heap
examples/l3-machine-code/**/*-heap
*Script_ttt.sml