src/HOL/Library/Old_Datatype.thy
changeset 61585 a9599d3d7610
parent 60500 903bb1495239
child 61943 7fba644ed827
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    morphisms Rep_Node Abs_Node
     1.5    unfolding Node_def by auto
     1.6  
     1.7 -text\<open>Datatypes will be represented by sets of type @{text node}\<close>
     1.8 +text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close>
     1.9  
    1.10  type_synonym 'a item        = "('a, unit) node set"
    1.11  type_synonym ('a, 'b) dtree = "('a, 'b) node set"