equal
deleted
inserted
replaced
193 and notnot: "-- (-- x) = x" |
193 and notnot: "-- (-- x) = x" |
194 defines "x || y == --(-- x && -- y)" |
194 defines "x || y == --(-- x && -- y)" |
195 begin |
195 begin |
196 |
196 |
197 thm lor_def |
197 thm lor_def |
198 (* Can we get rid the the additional hypothesis, caused by Local_Theory.notes? *) |
|
199 |
198 |
200 lemma "x || y = --(-- x && --y)" |
199 lemma "x || y = --(-- x && --y)" |
201 by (unfold lor_def) (rule refl) |
200 by (unfold lor_def) (rule refl) |
202 |
201 |
203 end |
202 end |