Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-02-12

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

All times shown according to UTC.

Time Nick Message
23:39 crc_ joined #isabelle
23:41 crc_ I'm a noob trying to prove nat commutivity without using "apply(auto)". I have it down to "Suc (add (Suc n) m) = add (Suc n) (Suc m)" which is the definition of "add". How do I complete the proof? I'm looking for something like "apply(by_definition add)"
23:59 tangentstorm you can use the definition as a simplification rule
23:59 tangentstorm or at least i think you can

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