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.
Tuned some comments.
authorberghofe
Tue, 17 Aug 1999 14:01:39 +0200
changeset 7228 ddb67dcf026c
parent 7227 a8e86b8e6fd1
child 7229 6773ba0c36d5
Tuned some comments.
src/HOL/Tools/datatype_abs_proofs.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/datatype_rep_proofs.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Aug 17 14:00:30 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Aug 17 14:01:39 1999 +0200
@@ -10,7 +10,6 @@
  - case distinction (exhaustion) theorems
  - characteristic equations for primrec combinators
  - characteristic equations for case combinators
- - distinctness of constructors (external version)
  - equations for splitting "P (case ...)" expressions
  - datatype size function
  - "nchotomy" and "case_cong" theorems for TFL
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Aug 17 14:00:30 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Aug 17 14:01:39 1999 +0200
@@ -7,7 +7,7 @@
 Proof of characteristic theorems:
 
  - injectivity of constructors
- - distinctness of constructors (internal version)
+ - distinctness of constructors
  - induction theorem
 
 *)
isabelle