src/HOLCF/Tutorial/Domain_ex.thy

--- a/src/HOLCF/Tutorial/Domain_ex.thy	Sun Oct 24 15:19:17 2010 -0700
+++ b/src/HOLCF/Tutorial/Domain_ex.thy	Sun Oct 24 15:42:57 2010 -0700
@@ -140,9 +140,9 @@
 thm tree.injects
 
 text {* Rules about case combinator *}
-term tree_when
-thm tree.tree_when_def
-thm tree.when_rews
+term tree_case
+thm tree.tree_case_def
+thm tree.case_rews
 
 text {* Rules about selectors *}
 term left