equal
deleted
inserted
replaced
188 apply(rule ccontr) |
188 apply(rule ccontr) |
189 apply(erule_tac x="a" in allE) |
189 apply(erule_tac x="a" in allE) |
190 apply simp |
190 apply simp |
191 done |
191 done |
192 |
192 |
193 instantiation loc' :: equal begin |
193 instantiation loc' :: equal |
|
194 begin |
|
195 |
194 definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'" |
196 definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'" |
195 instance proof qed(simp add: equal_loc'_def) |
197 instance by default (simp add: equal_loc'_def) |
|
198 |
196 end |
199 end |
197 |
200 |
198 end |
201 end |