isabelle: src/HOL/Import/Generate-HOL/ROOT.ML@ac272926fb77 (annotated)

14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	1	(* Title: HOL/Import/Generate-HOL/ROOT.ML
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	2	ID: $Id$
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	3	Author: Sebastian Skalberg (TU Muenchen)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	4	*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	5
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6	with_path ".." use_thy "HOL4Compat";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	with_path ".." use_thy "HOL4Syntax";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	use_thy "GenHOL4Prob";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	use_thy "GenHOL4Vec";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10	use_thy "GenHOL4Word32";