use proof objects for HOL by default
authorkleing
Wed, 14 May 2003 15:22:37 +0200
changeset 14029 fe031a7c75bc
parent 14028 ff6eb32b30a1
child 14030 cd928c0ac225
use proof objects for HOL by default
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed May 14 14:20:55 2003 +0200
+++ b/src/HOL/IsaMakefile	Wed May 14 15:22:37 2003 +0200
@@ -109,8 +109,7 @@
   Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
   document/root.tex hologic.ML meson_lemmas.ML simpdata.ML thy_syntax.ML
-	@$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL
-
+	@$(ISATOOL) usedir -b -g true -p 2 $(OUT)/Pure HOL
 
 
 ## HOL-Complex-HahnBanach