src/HOL/IsaMakefile
changeset 12410 ef373ec6ade8
parent 12396 2298d5b8e530
child 12432 90b0fc84f8d9
equal deleted inserted replaced
12409:25bf458af885 12410:ef373ec6ade8
   104   Transitive_Closure.thy Transitive_Closure_lemmas.ML Typedef.thy \
   104   Transitive_Closure.thy Transitive_Closure_lemmas.ML Typedef.thy \
   105   Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   105   Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   106   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
   106   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
   107   document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \
   107   document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \
   108   simpdata.ML subset.ML thy_syntax.ML
   108   simpdata.ML subset.ML thy_syntax.ML
   109 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
   109 	@$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL
   110 
   110 
   111 
   111 
   112 ## HOL-Real
   112 ## HOL-Real
   113 
   113 
   114 HOL-Real: HOL $(OUT)/HOL-Real
   114 HOL-Real: HOL $(OUT)/HOL-Real