Changed syntax of rep_datatype.
--- 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
--- a/src/HOL/Nat.thy Wed Oct 21 16:38:46 1998 +0200
+++ b/src/HOL/Nat.thy Wed Oct 21 17:38:47 1998 +0200
@@ -12,8 +12,8 @@
DatatypePackage.setup
rep_datatype nat
- distinct "[[Suc_not_Zero, Zero_not_Suc]]"
- inject "[[Suc_Suc_eq]]"
+ distinct Suc_not_Zero, Zero_not_Suc
+ inject Suc_Suc_eq
induct nat_induct
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)