# HG changeset patch
# User wenzelm
# Date 1127948343 -7200
# Node ID 9a13e0abdb8275e652607b1894ab9c7b121777ed
# Parent  299eeb303f049ed7e9fedea31541695cf107625b
HOL4 image is back;

diff -r 299eeb303f04 -r 9a13e0abdb82 src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Thu Sep 29 00:59:02 2005 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Thu Sep 29 00:59:03 2005 +0200
@@ -3,5 +3,5 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-use_thy "HOL4Prob";
-use_thy "HOL4";
+setmp quick_and_dirty true use_thy "HOL4Prob";
+setmp quick_and_dirty true use_thy "HOL4";
diff -r 299eeb303f04 -r 9a13e0abdb82 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 29 00:59:02 2005 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 29 00:59:03 2005 +0200
@@ -6,7 +6,7 @@
 
 default: HOL
 generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
-images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA
+images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA HOL4
 
 #Note: keep targets sorted (except for HOL-Library)
 test: \