src/HOL/IsaMakefile
changeset 26748 4d51ddd6aa5c
parent 26737 3d46c55f03af
child 26878 1aeac4d6b377
--- a/src/HOL/IsaMakefile	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 25 15:30:33 2008 +0200
@@ -92,7 +92,7 @@
   $(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML	\
   $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
   $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
-  Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
+  Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
   Divides.thy Equiv_Relations.thy Extraction.thy	\
   Finite_Set.thy Fun.thy FunDef.thy HOL.thy		\
   Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy	\
@@ -142,8 +142,8 @@
   Tools/sat_funcs.ML Tools/sat_solver.ML Tools/specification_package.ML	\
   Tools/split_rule.ML Tools/string_syntax.ML Tools/typecopy_package.ML	\
   Tools/typedef_codegen.ML Tools/typedef_package.ML			\
-  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
-  Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML	\
+  Transitive_Closure.thy Typedef.thy Wellfounded.thy		\
+  arith_data.ML document/root.tex hologic.ML	\
   int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL