--- a/Sum.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/Sum.thy Thu Mar 17 17:02:49 1994 +0100
@@ -7,17 +7,23 @@
*)
Sum = Prod +
-types "+" 2 (infixl 10)
-arities "+" :: (term,term)term
+
+types
+ ('a,'b) "+" (infixl 10)
+
+arities
+ "+" :: (term,term)term
+
consts
- Inl_Rep :: "['a,'a,'b,bool] => bool"
- Inr_Rep :: "['b,'a,'b,bool] => bool"
- Sum :: "(['a,'b,bool] => bool)set"
- Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)"
- Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b"
- Inl :: "'a => 'a+'b"
- Inr :: "'b => 'a+'b"
- sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+ Inl_Rep :: "['a,'a,'b,bool] => bool"
+ Inr_Rep :: "['b,'a,'b,bool] => bool"
+ Sum :: "(['a,'b,bool] => bool)set"
+ Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)"
+ Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b"
+ Inl :: "'a => 'a+'b"
+ Inr :: "'b => 'a+'b"
+ sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+
rules
Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)"
Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)"