Camelia, the Perl 6 bug

IRC log for #isabelle, 2011-12-22

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
00:26 eyebloom context is a keyword in isabelle....
00:27 eyebloom I just discovered
01:29 eyebloom joined #isabelle
05:58 eyebloom If I'm trying to proove something and I end up with Something ==> False, this means the thing I'm trying to proove is false. Correct?
05:59 eyebloom Or more precisely one of the subgoals resolves to that.
10:32 larsrh x ==> False is equivalent to ~x (not x)
10:32 larsrh your lemma doesn't have to be false; your proof steps might have been disadvantageous
10:33 larsrh or it's just ~x what you have to prove
11:18 tomprince joined #isabelle
14:40 eyebloom thanks
18:20 eyebloom joined #isabelle
19:32 eyebloom joined #isabelle
22:16 eyebloom joined #isabelle
22:19 eyebloom joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary