Changed syntax of rep_datatype.
authorberghofe
Wed Oct 21 17:38:47 1998 +0200 (1998-10-21)
changeset 5714b4f2e281a907
parent 5713 27d4fcf5fe5f
child 5715 5fc697ad232b
Changed syntax of rep_datatype.
src/HOL/Datatype.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Datatype.thy	Wed Oct 21 16:38:46 1998 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Oct 21 17:38:47 1998 +0200
     1.3 @@ -7,13 +7,12 @@
     1.4  Datatype = Univ +
     1.5  
     1.6  rep_datatype sum
     1.7 -  distinct "[[Inl_not_Inr, Inr_not_Inl]]"
     1.8 -  inject   "[[Inl_eq, Inr_eq]]"
     1.9 +  distinct Inl_not_Inr, Inr_not_Inl
    1.10 +  inject   Inl_eq, Inr_eq
    1.11    induct   sum_induct
    1.12  
    1.13  rep_datatype prod
    1.14 -  distinct "[[]]"
    1.15 -  inject   "[[Pair_eq]]"
    1.16 -  induct   "allI RS (allI RS (split_paired_All RS iffD2)) RS spec"
    1.17 +  inject   Pair_eq
    1.18 +  induct   prod_induct
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Nat.thy	Wed Oct 21 16:38:46 1998 +0200
     2.2 +++ b/src/HOL/Nat.thy	Wed Oct 21 17:38:47 1998 +0200
     2.3 @@ -12,8 +12,8 @@
     2.4    DatatypePackage.setup
     2.5  
     2.6  rep_datatype nat
     2.7 -  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
     2.8 -  inject   "[[Suc_Suc_eq]]"
     2.9 +  distinct Suc_not_Zero, Zero_not_Suc
    2.10 +  inject   Suc_Suc_eq
    2.11    induct   nat_induct
    2.12  
    2.13  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)