2009-10-17 Further in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:20:56 +0200] rev 120
Further in the proof
2009-10-17 compose_tac works with the full instantiation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 11:54:50 +0200] rev 119
compose_tac works with the full instantiation.
2009-10-17 slightly simplified get_fun function
Christian Urban <urbanc@in.tum.de> [Sat, 17 Oct 2009 12:19:06 +0200] rev 118
slightly simplified get_fun function
2009-10-17 The instantiated version is the same modulo beta
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:40:54 +0200] rev 117
The instantiated version is the same modulo beta
2009-10-17 Fully manually instantiated. Still fails...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:07:52 +0200] rev 116
Fully manually instantiated. Still fails...
2009-10-17 Little progress with match/instantiate
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 09:04:24 +0200] rev 115
Little progress with match/instantiate
2009-10-16 Fighting with the instantiation
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 19:21:05 +0200] rev 114
Fighting with the instantiation
2009-10-16 Symmetric version of REP_ABS_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 17:05:52 +0200] rev 113
Symmetric version of REP_ABS_RSP
2009-10-16 Progressing with the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 16:51:01 +0200] rev 112
Progressing with the proof
2009-10-16 Finally fix get_fun.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 10:54:31 +0200] rev 111
Finally fix get_fun.
2009-10-16 A fix for one fun_map; doesn't work for more.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 08:48:56 +0200] rev 110
A fix for one fun_map; doesn't work for more.
2009-10-16 fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de> [Fri, 16 Oct 2009 03:26:54 +0200] rev 109
fixed the problem with function types; but only type_of works; cterm_of does not work
2009-10-15 Description of the problem with get_fun.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 16:51:24 +0200] rev 108
Description of the problem with get_fun.
2009-10-15 A proper build_goal_term function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 16:36:20 +0200] rev 107
A proper build_goal_term function.
2009-10-15 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 12:06:00 +0200] rev 106
Cleaning the code
2009-10-15 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:57:33 +0200] rev 105
Merged
2009-10-15 Cleaning the proofs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:56:30 +0200] rev 104
Cleaning the proofs
2009-10-15 Cleaning the code, part 4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:55:52 +0200] rev 103
Cleaning the code, part 4
2009-10-15 slightly improved tyRel
Christian Urban <urbanc@in.tum.de> [Thu, 15 Oct 2009 11:53:11 +0200] rev 102
slightly improved tyRel
2009-10-15 Reordering the code, part 3
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:42:14 +0200] rev 101
Reordering the code, part 3
2009-10-15 Reordering the code, part 2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:29:38 +0200] rev 100
Reordering the code, part 2.
2009-10-15 Reordering the code, part 1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:25:25 +0200] rev 99
Reordering the code, part 1.
2009-10-15 Minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:20:50 +0200] rev 98
Minor cleaning.
2009-10-15 The definition of Fold1
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:17:27 +0200] rev 97
The definition of Fold1
2009-10-15 A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 10:25:23 +0200] rev 96
A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-14 Proving the proper RepAbs version
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 18:13:16 +0200] rev 95
Proving the proper RepAbs version
2009-10-14 Forgot to save, second part of the commit
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 16:23:49 +0200] rev 94
Forgot to save, second part of the commit
2009-10-14 Manually regularized list_induct2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 16:23:32 +0200] rev 93
Manually regularized list_induct2
2009-10-14 Fixed bug in regularise types. Now we can regularise list.induct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 12:05:39 +0200] rev 92
Fixed bug in regularise types. Now we can regularise list.induct.
2009-10-14 Function for checking recursively if lifting is needed
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 11:23:55 +0200] rev 91
Function for checking recursively if lifting is needed
2009-10-14 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 09:50:13 +0200] rev 90
Merge
2009-10-14 Proper handling of non-lifted quantifiers, testing type freezing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 09:47:16 +0200] rev 89
Proper handling of non-lifted quantifiers, testing type freezing.
2009-10-13 slight simplification of atomize_thm
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 22:22:15 +0200] rev 88
slight simplification of atomize_thm
2009-10-13 atomize_thm and meta_quantify.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 18:01:54 +0200] rev 87
atomize_thm and meta_quantify.
2009-10-13 Regularizing HOL all.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 13:37:07 +0200] rev 86
Regularizing HOL all.
2009-10-13 ":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:38:35 +0200] rev 85
":" is used for being in a set, "IN" means something else...
2009-10-13 First (untested) version of regularize for abstractions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:03:55 +0200] rev 84
First (untested) version of regularize for abstractions.
2009-10-13 restored old version
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 09:26:19 +0200] rev 83
restored old version
2009-10-12 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 00:02:22 +0200] rev 82
tuned
2009-10-12 slightly modified the parser
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:39:14 +0200] rev 81
slightly modified the parser
2009-10-12 deleted diagnostic code
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:16:20 +0200] rev 80
deleted diagnostic code
2009-10-12 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:06:14 +0200] rev 79
added quotient command (you need to update isar-keywords-prove.el)
2009-10-12 added new keyword
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 22:44:16 +0200] rev 78
added new keyword
2009-10-12 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 16:31:29 +0200] rev 77
Bounded quantifier
2009-10-12 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 15:47:27 +0200] rev 76
The tyREL function.
2009-10-12 started some strange functions
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 14:30:50 +0200] rev 75
started some strange functions
2009-10-12 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 13:58:31 +0200] rev 74
Further with the manual proof
2009-10-09 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 17:05:45 +0200] rev 73
Further experiments with proving induction manually
2009-10-09 Testing if I can prove the regularized version of 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
2009-10-08 exported parts of QuotMain into a separate ML-file
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
2009-10-06 consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
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.
2009-10-06 simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
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)
2009-10-06 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:41:35 +0200] rev 68
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
2009-10-06 tuned; nothing serious
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:36:08 +0200] rev 67
tuned; nothing serious
2009-10-06 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 09:28:59 +0200] rev 66
another improvement to unlam_def
2009-10-06 one further 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
2009-10-05 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 01:50:13 +0200] rev 64
simplified the unlam_def function
2009-10-05 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: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)
2009-10-05 used prop_of to get the term of a theorem (replaces crep_thm)
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)
2009-10-02 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:10:21 +0200] rev 61
Merged
2009-10-02 First theorem with quantifiers. Learned how to use sledgehammer.
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.
2009-10-01 simplified the storage of the map-functions by using TheoryDataFun
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
2009-09-30 Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
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'.
2009-09-29 used new cong_tac
Christian Urban <urbanc@in.tum.de> [Tue, 29 Sep 2009 22:35:48 +0200] rev 57
used new cong_tac
2009-09-29 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 17:46:18 +0200] rev 56
First version of handling of the universal quantifier
2009-09-29 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 15:58:14 +0200] rev 55
Handling abstraction correctly.
2009-09-29 second test
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:38:27 +0200] rev 54
second test
2009-09-29 Test line
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:24:57 +0200] rev 53
Test line
2009-09-29 Partially fix lifting of card_suc. The quantified variable still needs to be changed.
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.
2009-09-29 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 10:49:31 +0200] rev 51
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
2009-09-29 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:58:02 +0200] rev 50
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
2009-09-29 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:26:22 +0200] rev 49
Merged
2009-09-28 added name to prove
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 23:17:29 +0200] rev 48
added name to prove
2009-09-28 consistent state
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 19:24:55 +0200] rev 47
consistent state
2009-09-28 some tuning of my code
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 19:22:28 +0200] rev 46
some tuning of my code
2009-09-28 Cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 19:15:19 +0200] rev 45
Cleanup
2009-09-28 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 19:10:27 +0200] rev 44
Merged
2009-09-28 Cleaning the code with Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 18:59:04 +0200] rev 43
Cleaning the code with Makarius
2009-09-28 Instnatiation with a schematic variable
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 15:37:38 +0200] rev 42
Instnatiation with a schematic variable
2009-09-28 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 02:39:44 +0200] rev 41
added ctxt as explicit argument to build_goal; tuned
2009-09-25 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 19:26:18 +0200] rev 40
slightly tuned the comment for unlam
2009-09-25 fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 17:08:50 +0200] rev 39
fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
2009-09-25 tuned slightly one proof
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 16:50:11 +0200] rev 38
tuned slightly one proof
2009-09-25 A version of the tactic that exports variables correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 25 Sep 2009 14:50:35 +0200] rev 37
A version of the tactic that exports variables correctly. It still does not know how to instantiate the obtained theorems.
2009-09-25 Minor cleaning: whitespace, commas etc.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 25 Sep 2009 09:38:16 +0200] rev 36
Minor cleaning: whitespace, commas etc.
2009-09-24 Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 17:43:26 +0200] rev 35
Correctly handling abstractions while building goals Use DatatypeAux cong_tac instead of own functions since it handles universal quantifiers properly.
2009-09-24 Minor cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 13:32:52 +0200] rev 34
Minor cleanup
2009-09-24 Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 11:38:20 +0200] rev 33
Found the source for the exception and added a handle for it.
2009-09-24 Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 09:09:46 +0200] rev 32
Make the tactic use Trueprop_cong and atomize.
2009-09-23 Proper code for getting the prop out of the theorem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 23 Sep 2009 16:57:56 +0200] rev 31
Proper code for getting the prop out of the theorem.
2009-09-23 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 23 Sep 2009 16:44:56 +0200] rev 30
Using "atomize" the versions with arbitrary Trueprops can be proven.
2009-09-22 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 22 Sep 2009 17:39:52 +0200] rev 29
Proper definition of CARD and some properties of it. Translation should now support Pure assumptions and Trueprops anywhere, but a problem needs to be fixed with the tactic.
2009-09-22 some comments
Christian Urban <urbanc@in.tum.de> [Tue, 22 Sep 2009 09:42:27 +0200] rev 28
some comments
2009-09-21 merged
Christian Urban <urbanc@in.tum.de> [Mon, 21 Sep 2009 18:18:29 +0200] rev 27
merged
2009-09-21 slight tuning
Christian Urban <urbanc@in.tum.de> [Mon, 21 Sep 2009 18:18:01 +0200] rev 26
slight tuning
2009-09-21 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 21 Sep 2009 16:45:44 +0200] rev 25
The tactic with REPEAT, CHANGED and a proper simpset.
2009-09-21 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 21 Sep 2009 10:53:01 +0200] rev 24
Merged with my changes from the morning: further working on the tactic and produced goals.
2009-09-20 some more beautification
Ning@localhost [Sun, 20 Sep 2009 05:48:49 +0100] rev 23
some more beautification
2009-09-20 beautification of some proofs
Ning@localhost [Sun, 20 Sep 2009 05:18:36 +0100] rev 22
beautification of some proofs
2009-09-18 Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 18 Sep 2009 17:30:33 +0200] rev 21
Added more useful quotient facts.
2009-09-18 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 18 Sep 2009 13:44:06 +0200] rev 20
Testing the tactic further.
2009-09-17 The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 17 Sep 2009 16:55:11 +0200] rev 19
The tactic still only for fset
2009-09-17 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 17 Sep 2009 12:06:06 +0200] rev 18
Infrastructure for the tactic
2009-09-16 More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 16 Sep 2009 11:50:41 +0200] rev 17
More naming/binding suggestions from Makarius
2009-09-15 Code cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 11:31:35 +0200] rev 16
Code cleanup
2009-09-15 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 10:00:34 +0200] rev 15
Cleaning the code
2009-09-15 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 09:59:56 +0200] rev 14
Generalized interpretation, works for all examples.
2009-08-28 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 28 Aug 2009 17:12:19 +0200] rev 13
Fixes after suggestions from Makarius: - indentation - lowercase/uppercase - axioms -> axiomatization - proper operator priorities - proper exception handling
2009-08-28 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 28 Aug 2009 10:01:25 +0200] rev 12
More examples.
2009-08-27 Use metavariables in the 'non-lambda' definitions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 Aug 2009 09:04:39 +0200] rev 11
Use metavariables in the 'non-lambda' definitions
2009-08-26 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 Aug 2009 11:31:55 +0200] rev 10
Make both kinds of definitions.
2009-08-25 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 17:37:50 +0200] rev 9
Changed to the use of "modern interface" (removed the _cmd and passing of strings) Fixed Trueprop handling and the first proof starts working properly.
2009-08-25 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 14:37:11 +0200] rev 8
Initial version of the function that builds goals.
2009-08-25 - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 10:35:28 +0200] rev 7
- Build an interpretation for fset from ML level and use it - Added CARD
2009-08-24 added the prove command
Christian Urban <urbanc@in.tum.de> [Tue, 25 Aug 2009 00:30:23 +0200] rev 6
added the prove command
2009-08-21 Fixed
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 Aug 2009 13:56:20 +0200] rev 5
Fixed
2009-08-21 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 21 Aug 2009 13:36:58 +0200] rev 4
tuned
2009-08-20 UNION - Append theorem
cek@localhost.localdomain [Thu, 20 Aug 2009 14:44:29 +0200] rev 3
UNION - Append theorem
2009-08-20 update
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 10:31:44 +0200] rev 2
update
2009-08-18 updated slightly
Christian Urban <urbanc@in.tum.de> [Tue, 18 Aug 2009 14:04:51 +0200] rev 1
updated slightly
2009-08-11 initial commit
Christian Urban <urbanc@in.tum.de> [Tue, 11 Aug 2009 12:29:15 +0200] rev 0
initial commit
(0) +480 +1000 +3000 tip