src/HOL/Datatype.thy
changeset 5714 b4f2e281a907
parent 5181 4ba3787d9709
child 5759 bf5d9e5b8cdf
--- a/src/HOL/Datatype.thy	Wed Oct 21 16:38:46 1998 +0200
+++ b/src/HOL/Datatype.thy	Wed Oct 21 17:38:47 1998 +0200
@@ -7,13 +7,12 @@
 Datatype = Univ +
 
 rep_datatype sum
-  distinct "[[Inl_not_Inr, Inr_not_Inl]]"
-  inject   "[[Inl_eq, Inr_eq]]"
+  distinct Inl_not_Inr, Inr_not_Inl
+  inject   Inl_eq, Inr_eq
   induct   sum_induct
 
 rep_datatype prod
-  distinct "[[]]"
-  inject   "[[Pair_eq]]"
-  induct   "allI RS (allI RS (split_paired_All RS iffD2)) RS spec"
+  inject   Pair_eq
+  induct   prod_induct
 
 end