equal
deleted
inserted
replaced
64 |
64 |
65 |
65 |
66 section "type and expression names" |
66 section "type and expression names" |
67 |
67 |
68 (** unfortunately cannot simply instantiate tnam **) |
68 (** unfortunately cannot simply instantiate tnam **) |
69 datatype tnam' = HasFoo' | Base' | Ext' | Main' |
69 datatype_new tnam' = HasFoo' | Base' | Ext' | Main' |
70 datatype vnam' = arr' | vee' | z' | e' |
70 datatype_new vnam' = arr' | vee' | z' | e' |
71 datatype label' = lab1' |
71 datatype_new label' = lab1' |
72 |
72 |
73 axiomatization |
73 axiomatization |
74 tnam' :: "tnam' \<Rightarrow> tnam" and |
74 tnam' :: "tnam' \<Rightarrow> tnam" and |
75 vnam' :: "vnam' \<Rightarrow> vname" and |
75 vnam' :: "vnam' \<Rightarrow> vname" and |
76 label':: "label' \<Rightarrow> label" |
76 label':: "label' \<Rightarrow> label" |