Wed, 29 Sep 2010 06:45:01 -0400 use also induct_schema for the Let-example (permute_bn is used)
Christian Urban <urbanc@in.tum.de> [Wed, 29 Sep 2010 06:45:01 -0400] rev 2498
use also induct_schema for the Let-example (permute_bn is used)
Wed, 29 Sep 2010 04:42:37 -0400 test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de> [Wed, 29 Sep 2010 04:42:37 -0400] rev 2497
test with induct_schema for simpler strong_ind proofs
Wed, 29 Sep 2010 16:36:31 +0900 substitution definition with 'next_name'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 29 Sep 2010 16:36:31 +0900] rev 2496
substitution definition with 'next_name'.
Tue, 28 Sep 2010 08:21:47 -0400 merged
Christian Urban <urbanc@in.tum.de> [Tue, 28 Sep 2010 08:21:47 -0400] rev 2495
merged
(0) -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 tip