src/HOL/Import/ROOT.ML
author wenzelm
Wed, 15 Apr 2009 11:14:48 +0200
changeset 30895 bad26d8f0adf
parent 25374 7657a081fcb4
child 37296 1fad5b94c0ae
permissions -rw-r--r--
updated for Isabelle2009;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14620
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     1
(*  Title:      HOL/Import/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
25374
7657a081fcb4 qualified Proofterm.proofs;
wenzelm
parents: 17624
diff changeset
     6
Proofterm.proofs := 0;
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
use_thy "HOL4Compat";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
use_thy "HOL4Syntax";