| changeset 67399 | eab6ce8368fa |
| parent 67091 | 1393c2340eec |
| child 67729 | 5152afa6258f |
| 67398:5eb932e604a2 | 67399:eab6ce8368fa |
|---|---|
337 end |
337 end |
338 |
338 |
339 instantiation literal :: equal |
339 instantiation literal :: equal |
340 begin |
340 begin |
341 |
341 |
342 lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" . |
342 lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "(=)" . |
343 |
343 |
344 instance by intro_classes (transfer, simp) |
344 instance by intro_classes (transfer, simp) |
345 |
345 |
346 end |
346 end |
347 |
347 |