Mon, 21 Sep 2009 18:18:29 +0200 |
Christian Urban |
merged
|
file |
diff |
annotate
|
Mon, 21 Sep 2009 18:18:01 +0200 |
Christian Urban |
slight tuning
|
file |
diff |
annotate
|
Mon, 21 Sep 2009 16:45:44 +0200 |
Cezary Kaliszyk |
The tactic with REPEAT, CHANGED and a proper simpset.
|
file |
diff |
annotate
|
Mon, 21 Sep 2009 10:53:01 +0200 |
Cezary Kaliszyk |
Merged with my changes from the morning:
|
file |
diff |
annotate
|
Sun, 20 Sep 2009 05:48:49 +0100 |
Ning |
some more beautification
|
file |
diff |
annotate
|
Sun, 20 Sep 2009 05:18:36 +0100 |
Ning |
beautification of some proofs
|
file |
diff |
annotate
|
Fri, 18 Sep 2009 17:30:33 +0200 |
Cezary Kaliszyk |
Added more useful quotient facts.
|
file |
diff |
annotate
|
Fri, 18 Sep 2009 13:44:06 +0200 |
Cezary Kaliszyk |
Testing the tactic further.
|
file |
diff |
annotate
|
Thu, 17 Sep 2009 16:55:11 +0200 |
Cezary Kaliszyk |
The tactic still only for fset
|
file |
diff |
annotate
|
Thu, 17 Sep 2009 12:06:06 +0200 |
Cezary Kaliszyk |
Infrastructure for the tactic
|
file |
diff |
annotate
|
Wed, 16 Sep 2009 11:50:41 +0200 |
Cezary Kaliszyk |
More naming/binding suggestions from Makarius
|
file |
diff |
annotate
|
Tue, 15 Sep 2009 11:31:35 +0200 |
Cezary Kaliszyk |
Code cleanup
|
file |
diff |
annotate
|
Tue, 15 Sep 2009 10:00:34 +0200 |
Cezary Kaliszyk |
Cleaning the code
|
file |
diff |
annotate
|
Tue, 15 Sep 2009 09:59:56 +0200 |
Cezary Kaliszyk |
Generalized interpretation, works for all examples.
|
file |
diff |
annotate
|
Fri, 28 Aug 2009 17:12:19 +0200 |
Cezary Kaliszyk |
Fixes after suggestions from Makarius:
|
file |
diff |
annotate
|
Fri, 28 Aug 2009 10:01:25 +0200 |
Cezary Kaliszyk |
More examples.
|
file |
diff |
annotate
|
Thu, 27 Aug 2009 09:04:39 +0200 |
Cezary Kaliszyk |
Use metavariables in the 'non-lambda' definitions
|
file |
diff |
annotate
|
Wed, 26 Aug 2009 11:31:55 +0200 |
Cezary Kaliszyk |
Make both kinds of definitions.
|
file |
diff |
annotate
|
Tue, 25 Aug 2009 17:37:50 +0200 |
Cezary Kaliszyk |
Changed to the use of "modern interface"
|
file |
diff |
annotate
|
Tue, 25 Aug 2009 14:37:11 +0200 |
Cezary Kaliszyk |
Initial version of the function that builds goals.
|
file |
diff |
annotate
|
Tue, 25 Aug 2009 10:35:28 +0200 |
Cezary Kaliszyk |
- Build an interpretation for fset from ML level and use it
|
file |
diff |
annotate
|
Tue, 25 Aug 2009 00:30:23 +0200 |
Christian Urban |
added the prove command
|
file |
diff |
annotate
|
Fri, 21 Aug 2009 13:56:20 +0200 |
Cezary Kaliszyk |
Fixed
|
file |
diff |
annotate
|
Fri, 21 Aug 2009 13:36:58 +0200 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
Thu, 20 Aug 2009 14:44:29 +0200 |
cek |
UNION - Append theorem
|
file |
diff |
annotate
|
Thu, 20 Aug 2009 10:31:44 +0200 |
Christian Urban |
update
|
file |
diff |
annotate
|
Tue, 18 Aug 2009 14:04:51 +0200 |
Christian Urban |
updated slightly
|
file |
diff |
annotate
|
Tue, 11 Aug 2009 12:29:15 +0200 |
Christian Urban |
initial commit
|
file |
diff |
annotate
|