# HG changeset patch
# User haftmann
# Date 1156854672 -7200
# Node ID dc1e8c24a475c0dc77162a05933d9400d527eaea
# Parent  d5b4b55ad2778c6df90ff7eea8d5a5eee7dc30f7
added typecopy_package and some examples

diff -r d5b4b55ad277 -r dc1e8c24a475 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Aug 29 14:31:11 2006 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 29 14:31:12 2006 +0200
@@ -119,6 +119,7 @@
   Tools/res_clause.ML Tools/rewrite_hol_proof.ML	\
   Tools/sat_funcs.ML					\
   Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
+  Tools/typecopy_package.ML	\
   Tools/typedef_package.ML Tools/typedef_codegen.ML	\
   Transitive_Closure.ML Transitive_Closure.thy		\
   Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
@@ -641,7 +642,7 @@
   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/Codegenerator.thy ex/Commutative_RingEx.thy               \
+  ex/CodeOperationalEquality.thy ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
   ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
   ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\