# HG changeset patch
# User huffman
# Date 1287960177 25200
# Node ID b63e966564da4ff496c8ca97c65295e8d674fa7e
# Parent  20df78048db551181ac745897b300ab6640f552e
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'

diff -r 20df78048db5 -r b63e966564da src/HOLCF/Library/Stream.thy
--- a/src/HOLCF/Library/Stream.thy	Sun Oct 24 15:19:17 2010 -0700
+++ b/src/HOLCF/Library/Stream.thy	Sun Oct 24 15:42:57 2010 -0700
@@ -96,13 +96,13 @@
 
 
 (* ----------------------------------------------------------------------- *)
-(* theorems about stream_when                                              *)
+(* theorems about stream_case                                              *)
 (* ----------------------------------------------------------------------- *)
 
-section "stream_when"
+section "stream_case"
 
 
-lemma stream_when_strictf: "stream_when$UU$s=UU"
+lemma stream_case_strictf: "stream_case$UU$s=UU"
 by (cases s, auto)
 
 
diff -r 20df78048db5 -r b63e966564da src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Oct 24 15:19:17 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Oct 24 15:42:57 2010 -0700
@@ -411,7 +411,7 @@
 
     (* definition of case combinator *)
     local
-      val case_bind = Binding.suffix_name "_when" dbind;
+      val case_bind = Binding.suffix_name "_case" dbind;
       fun lambda_arg (lazy, v) t =
           (if lazy then mk_fup else I) (big_lambda v t);
       fun lambda_args []      t = mk_one_case t
@@ -938,7 +938,7 @@
           ((qualified "iso_rews"  , iso_rews    ), [simp]),
           ((qualified "nchotomy"  , [nchotomy]  ), []),
           ((qualified "exhaust"   , [exhaust]   ), [case_names, cases_type]),
-          ((qualified "when_rews" , cases       ), [simp]),
+          ((qualified "case_rews" , cases       ), [simp]),
           ((qualified "compacts"  , compacts    ), [simp]),
           ((qualified "con_rews"  , con_rews    ), [simp]),
           ((qualified "sel_rews"  , sel_thms    ), [simp]),
diff -r 20df78048db5 -r b63e966564da 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
diff -r 20df78048db5 -r b63e966564da src/HOLCF/Tutorial/Fixrec_ex.thy
--- a/src/HOLCF/Tutorial/Fixrec_ex.thy	Sun Oct 24 15:19:17 2010 -0700
+++ b/src/HOLCF/Tutorial/Fixrec_ex.thy	Sun Oct 24 15:42:57 2010 -0700
@@ -208,8 +208,8 @@
   "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
 by (subst repeat.simps, simp)+
 
-lemma llist_when_repeat [simp]:
-  "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
+lemma llist_case_repeat [simp]:
+  "llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
 by (subst repeat.simps, simp)
 
 text {*