# HG changeset patch
# User haftmann
# Date 1174913580 -7200
# Node ID 2f4c974147462a25276cd0b6dbbccfdd5f46bde6
# Parent  c986140356b8c02344582f090c73105d6349511f
cleaned up Library( and ex/

diff -r c986140356b8 -r 2f4c97414746 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 26 12:48:30 2007 +0200
+++ b/src/HOL/IsaMakefile	Mon Mar 26 14:53:00 2007 +0200
@@ -211,7 +211,8 @@
   Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \
   Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \
   Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
-  Library/SCT_Examples.thy Library/sct.ML
+  Library/SCT_Examples.thy Library/sct.ML \
+  Library/Pure_term.thy Library/Eval.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
 
@@ -618,7 +619,7 @@
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
   ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
   ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
-  ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			 	\
+  ex/Eval_examples.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
   ex/Codegenerator.thy ex/Codegenerator_Rat.thy                                 \
   ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy                             \
   ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy                     \