Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 16:31:29 +0200] rev 77
Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 15:47:27 +0200] rev 76
The tyREL function.
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 14:30:50 +0200] rev 75
started some strange functions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 13:58:31 +0200] rev 74
Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 17:05:45 +0200] rev 73
Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 15:03:43 +0200] rev 72
Testing if I can prove the regularized version of induction manually
Christian Urban <urbanc@in.tum.de> [Thu, 08 Oct 2009 14:27:50 +0200] rev 71
exported parts of QuotMain into a separate ML-file
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 15:11:30 +0200] rev 70
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
proof of atomize_eqv.
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:56:23 +0200] rev 69
simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:41:35 +0200] rev 68
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:36:08 +0200] rev 67
tuned; nothing serious
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 09:28:59 +0200] rev 66
another improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 02:02:51 +0200] rev 65
one further improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 01:50:13 +0200] rev 64
simplified the unlam_def function
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:54:02 +0200] rev 63
added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:24:32 +0200] rev 62
used prop_of to get the term of a theorem (replaces crep_thm)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:10:21 +0200] rev 61
Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:09:33 +0200] rev 60
First theorem with quantifiers. Learned how to use sledgehammer.
Christian Urban <urbanc@in.tum.de> [Thu, 01 Oct 2009 16:10:14 +0200] rev 59
simplified the storage of the map-functions by using TheoryDataFun
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 30 Sep 2009 16:57:09 +0200] rev 58
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Christian Urban <urbanc@in.tum.de> [Tue, 29 Sep 2009 22:35:48 +0200] rev 57
used new cong_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 17:46:18 +0200] rev 56
First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 15:58:14 +0200] rev 55
Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:38:27 +0200] rev 54
second test
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:24:57 +0200] rev 53
Test line
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 11:55:37 +0200] rev 52
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 10:49:31 +0200] rev 51
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:58:02 +0200] rev 50
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:26:22 +0200] rev 49
Merged
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 23:17:29 +0200] rev 48
added name to prove