Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changed syntax of rep_datatype.
authorberghofe
Wed, 21 Oct 1998 17:38:47 +0200
changeset 5714 b4f2e281a907
parent 5713 27d4fcf5fe5f
child 5715 5fc697ad232b
Changed syntax of rep_datatype.
src/HOL/Datatype.thy file | annotate | diff | comparison | revisions
src/HOL/Nat.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle