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