HOL4 image is back;
authorwenzelm
Thu Sep 29 00:59:03 2005 +0200 (2005-09-29)
changeset 177109a13e0abdb82
parent 17709 299eeb303f04
child 17711 c16cbe73798c
HOL4 image is back;
src/HOL/Import/HOL/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Import/HOL/ROOT.ML	Thu Sep 29 00:59:02 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Thu Sep 29 00:59:03 2005 +0200
     1.3 @@ -3,5 +3,5 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 -use_thy "HOL4Prob";
     1.8 -use_thy "HOL4";
     1.9 +setmp quick_and_dirty true use_thy "HOL4Prob";
    1.10 +setmp quick_and_dirty true use_thy "HOL4";
     2.1 --- a/src/HOL/IsaMakefile	Thu Sep 29 00:59:02 2005 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Thu Sep 29 00:59:03 2005 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  default: HOL
     2.6  generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
     2.7 -images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA
     2.8 +images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA HOL4
     2.9  
    2.10  #Note: keep targets sorted (except for HOL-Library)
    2.11  test: \