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.
compile
authorblanchet
Mon, 03 Sep 2012 11:54:21 +0200
changeset 49076 d2ed455fa3d2
parent 49075 ed769978dc8d
child 49094 7b6beb7e99c1
compile
src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Mon Sep 03 11:54:21 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy	Mon Sep 03 11:54:21 2012 +0200
@@ -15,7 +15,7 @@
 
 typedecl N  typedecl T
 
-bnf_codata Tree: 'Tree = "N \<times> (T + 'Tree) fset"
+codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset"
 
 
 section {* Sugar notations for Tree *}
isabelle