.gitignore

*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/index.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
*.tttsave
/TAGS