equal
deleted
inserted
replaced
109 "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" |
109 "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" |
110 "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
110 "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
111 "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool" |
111 "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool" |
112 "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool" |
112 "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool" |
113 |
113 |
114 subsection {* heavy use of names *} |
114 subsection {* heavy usage of names *} |
115 |
115 |
116 definition |
116 definition |
117 f :: nat |
117 f :: nat |
118 "f = 2" |
118 "f = 2" |
119 g :: nat |
119 g :: nat |