consistent interacitve bootstrap of HOL-Main
authorhaftmann
Fri Jan 25 14:53:58 2008 +0100 (2008-01-25)
changeset 25964080f89d89990
parent 25963 07e08dad8a77
child 25965 05df64f786a4
consistent interacitve bootstrap of HOL-Main
src/HOL/Main.thy
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/Main.thy	Fri Jan 25 14:53:56 2008 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Jan 25 14:53:58 2008 +0100
     1.3 @@ -15,4 +15,6 @@
     1.4  
     1.5  ML {* val HOL_proofs = ! Proofterm.proofs *}
     1.6  
     1.7 +ML {* path_add "~~/src/HOL/Library" *}
     1.8 +
     1.9  end
     2.1 --- a/src/HOL/ROOT.ML	Fri Jan 25 14:53:56 2008 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Fri Jan 25 14:53:58 2008 +0100
     2.3 @@ -5,5 +5,3 @@
     2.4  *)
     2.5  
     2.6  use_thy "Main";
     2.7 -
     2.8 -path_add "~~/src/HOL/Library";