--- a/src/HOL/Sum.thy Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Sum.thy Fri Mar 08 13:11:09 1996 +0100
@@ -10,13 +10,12 @@
(* type definition *)
-consts
+constdefs
Inl_Rep :: ['a, 'a, 'b, bool] => bool
- Inr_Rep :: ['b, 'a, 'b, bool] => bool
+ "Inl_Rep == (%a. %x y p. x=a & p)"
-defs
- Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)"
- Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)"
+ Inr_Rep :: ['b, 'a, 'b, bool] => bool
+ "Inr_Rep == (%b. %x y p. y=b & ~p)"
typedef (Sum)
('a, 'b) "+" (infixr 10)