src/HOL/Import/HOL/ROOT.ML
author skalberg
Fri Apr 02 17:37:45 2004 +0200 (2004-04-02)
changeset 14516 a183dec876ab
child 14620 1be590fd2422
permissions -rw-r--r--
Added HOL proof importer.
     1 with_path ".." use_thy "HOL4Compat";
     2 with_path ".." use_thy "HOL4Syntax";
     3 setmp quick_and_dirty true use_thy "HOL4Prob";
     4 setmp quick_and_dirty true use_thy "HOL4";