src/HOL/IsaMakefile
changeset 24994 c385c4eabb3b
parent 24915 fc90277c0dd7
child 25171 4a9c25bffc9b
--- a/src/HOL/IsaMakefile	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 12 08:21:09 2007 +0200
@@ -211,7 +211,7 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL \
   Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
   Library/Efficient_Nat.thy Library/Executable_Set.thy \
-  Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
+  Library/Infinite_Set.thy \
   Library/FuncSet.thy Library/Library.thy \
   Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
   Library/NatPair.thy \
@@ -231,8 +231,9 @@
   Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
   Library/SCT_Examples.thy Library/sct.ML \
   Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
-  Library/Pretty_Int.thy \
-  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy\
+  Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
+  Library/Code_Integer.thy Library/Code_Message.thy \
+  Library/Abstract_Rat.thy \
   Library/Numeral_Type.thy Library/Boolean_Algebra.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library