Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2014-07-10

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

All times shown according to UTC.

Time Nick Message
06:16 dmiles_afk joined #isabelle
06:36 dmiles_afk joined #isabelle
08:01 dmiles_afk joined #isabelle
14:11 safinaskar-i joined #isabelle
14:14 safinaskar-i how to do structural induction on type like 'datatype tree = node "tree list"'? logics-HOL.pdf says I should do induction using 'induct_tac "x1 x2" i', but how exactly to do this? please give me some example
14:48 safinaskar-i assume i have "datatype obj = nth_obj nat". how to prove "bij nth_obj"?
14:49 safinaskar-i maybe this is already proved?
15:22 safinaskar-i left #isabelle
22:33 ski joined #isabelle
22:33 leonweber1 joined #isabelle
22:34 dmiles_afk joined #isabelle
22:36 kini joined #isabelle
22:36 mal`` joined #isabelle

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