--- a/src/HOLCF/ex/Domain_ex.thy Wed Feb 24 14:20:07 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy Wed Feb 24 16:15:03 2010 -0800
@@ -122,7 +122,7 @@
text {* Rules about constructors *}
term Leaf
term Node
-thm tree.Leaf_def tree.Node_def
+thm Leaf_def Node_def
thm tree.exhaust
thm tree.casedist
thm tree.compacts
@@ -175,9 +175,11 @@
thm tree.finites
text {* Rules about bisimulation predicate *}
+(* COINDUCTION TEMPORARILY DISABLED
term tree_bisim
thm tree.bisim_def
thm tree.coind
+COINDUCTION TEMPORARILY DISABLED *)
text {* Induction rule *}
thm tree.ind