Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
case was renamed to sum_case
authornipkow
Wed, 26 Jan 1994 22:07:06 +0100
changeset 248 0d0a6a17a02f
parent 247 bc10568855ee
child 249 ec0b34154a6e
case was renamed to sum_case
src/HOLCF/Lift1.ML file | annotate | diff | comparison | revisions
src/HOLCF/Lift1.thy file | annotate | diff | comparison | revisions
src/HOLCF/lift1.ML file | annotate | diff | comparison | revisions
src/HOLCF/lift1.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Lift1.ML	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/Lift1.ML	Wed Jan 26 22:07:06 1994 +0100
@@ -71,7 +71,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -80,7 +80,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -91,7 +91,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac TrueI 1)
 	]);
 
@@ -104,8 +104,8 @@
 	(atac 2),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -115,8 +115,8 @@
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
--- a/src/HOLCF/Lift1.thy	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/Lift1.thy	Wed Jan 26 22:07:06 1994 +0100
@@ -40,14 +40,14 @@
   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
 
   Ilift_def     "Ilift(f)(x)==\
-\                case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
+\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
  
   less_lift_def "less_lift(x1)(x2) == \
-\          (case (Rep_Lift(x1))\
-\                (% y1.True)\
-\                (% y2.case (Rep_Lift(x2))\
-\                           (% z1.False)\
-\                           (% z2.y2<<z2)))"
+\          (sum_case (Rep_Lift(x1))\
+\                    (% y1.True)\
+\                    (% y2.sum_case (Rep_Lift(x2))\
+\                                   (% z1.False)\
+\                                   (% z2.y2<<z2)))"
 
 end
 
--- a/src/HOLCF/lift1.ML	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/lift1.ML	Wed Jan 26 22:07:06 1994 +0100
@@ -71,7 +71,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -80,7 +80,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -91,7 +91,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac TrueI 1)
 	]);
 
@@ -104,8 +104,8 @@
 	(atac 2),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -115,8 +115,8 @@
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
--- a/src/HOLCF/lift1.thy	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/lift1.thy	Wed Jan 26 22:07:06 1994 +0100
@@ -40,14 +40,14 @@
   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
 
   Ilift_def     "Ilift(f)(x)==\
-\                case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
+\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
  
   less_lift_def "less_lift(x1)(x2) == \
-\          (case (Rep_Lift(x1))\
-\                (% y1.True)\
-\                (% y2.case (Rep_Lift(x2))\
-\                           (% z1.False)\
-\                           (% z2.y2<<z2)))"
+\          (sum_case (Rep_Lift(x1))\
+\                    (% y1.True)\
+\                    (% y2.sum_case (Rep_Lift(x2))\
+\                                   (% z1.False)\
+\                                   (% z2.y2<<z2)))"
 
 end
isabelle