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.
removal of needless quotes
authorlcp
Tue, 06 Sep 1994 11:02:16 +0200
changeset 581 465075fd257b
parent 580 909e00299009
child 582 8f1f1fab70ad
removal of needless quotes
src/ZF/List.thy file | annotate | diff | comparison | revisions
src/ZF/ex/TF.thy file | annotate | diff | comparison | revisions 
--- a/src/ZF/List.thy	Wed Aug 31 17:34:12 1994 +0200
+++ b/src/ZF/List.thy	Tue Sep 06 11:02:16 1994 +0200
@@ -30,7 +30,7 @@
 
   
 datatype
-  "list(A)" = "Nil" | "Cons" ("a:A", "l: list(A)")
+  "list(A)" = Nil | Cons ("a:A", "l: list(A)")
 
 
 translations
--- a/src/ZF/ex/TF.thy	Wed Aug 31 17:34:12 1994 +0200
+++ b/src/ZF/ex/TF.thy	Tue Sep 06 11:02:16 1994 +0200
@@ -18,9 +18,9 @@
   tree, forest, tree_forest    :: "i=>i"
 
 datatype
-  "tree(A)"   = "Tcons" ("a: A",  "f: forest(A)")
+  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
 and
-  "forest(A)" = "Fnil"  |  "Fcons" ("t: tree(A)",  "f: forest(A)")
+  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
 
 rules
   TF_rec_def
isabelle