wenzelm [Fri, 13 Jan 2006 01:12:58 +0100] rev 18662
ProofContext.def_export;
urbanc [Wed, 11 Jan 2006 18:46:31 +0100] rev 18661
updated to new induction principle
urbanc [Wed, 11 Jan 2006 18:39:19 +0100] rev 18660
cahges to use the new induction-principle (now proved in
full glory)
urbanc [Wed, 11 Jan 2006 18:38:32 +0100] rev 18659
changes to make use of the new induction principle proved by
Stefan horay (hooraayyy)
berghofe [Wed, 11 Jan 2006 18:21:23 +0100] rev 18658
Implemented proof of (strong) induction rule.
berghofe [Wed, 11 Jan 2006 18:20:59 +0100] rev 18657
Added theorem at_finite_select.
urbanc [Wed, 11 Jan 2006 17:12:30 +0100] rev 18656
added lemmas perm_empty, perm_insert to do with
permutations on sets
urbanc [Wed, 11 Jan 2006 17:10:11 +0100] rev 18655
merged the silly lemmas into the eqvt proof of subtype
urbanc [Wed, 11 Jan 2006 17:07:57 +0100] rev 18654
tuned proofs
urbanc [Wed, 11 Jan 2006 14:00:11 +0100] rev 18653
tuned the eqvt-proof