2009-09-28 |
Christian Urban |
consistent state
|
file |
diff |
annotate
|
2009-09-28 |
Christian Urban |
some tuning of my code
|
file |
diff |
annotate
|
2009-09-28 |
Cezary Kaliszyk |
Cleanup
|
file |
diff |
annotate
|
2009-09-28 |
Cezary Kaliszyk |
Merged
|
file |
diff |
annotate
|
2009-09-28 |
Cezary Kaliszyk |
Cleaning the code with Makarius
|
file |
diff |
annotate
|
2009-09-28 |
Cezary Kaliszyk |
Instnatiation with a schematic variable
|
file |
diff |
annotate
|
2009-09-28 |
Christian Urban |
added ctxt as explicit argument to build_goal; tuned
|
file |
diff |
annotate
|
2009-09-25 |
Christian Urban |
slightly tuned the comment for unlam
|
file |
diff |
annotate
|
2009-09-25 |
Christian Urban |
fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
|
file |
diff |
annotate
|
2009-09-25 |
Christian Urban |
tuned slightly one proof
|
file |
diff |
annotate
|
2009-09-25 |
Cezary Kaliszyk |
A version of the tactic that exports variables correctly.
|
file |
diff |
annotate
|
2009-09-25 |
Cezary Kaliszyk |
Minor cleaning: whitespace, commas etc.
|
file |
diff |
annotate
|
2009-09-24 |
Cezary Kaliszyk |
Correctly handling abstractions while building goals
|
file |
diff |
annotate
|
2009-09-24 |
Cezary Kaliszyk |
Minor cleanup
|
file |
diff |
annotate
|
2009-09-24 |
Cezary Kaliszyk |
Found the source for the exception and added a handle for it.
|
file |
diff |
annotate
|
2009-09-24 |
Cezary Kaliszyk |
Make the tactic use Trueprop_cong and atomize.
|
file |
diff |
annotate
|
2009-09-23 |
Cezary Kaliszyk |
Proper code for getting the prop out of the theorem.
|
file |
diff |
annotate
|
2009-09-23 |
Cezary Kaliszyk |
Using "atomize" the versions with arbitrary Trueprops can be proven.
|
file |
diff |
annotate
|
2009-09-22 |
Cezary Kaliszyk |
Proper definition of CARD and some properties of it.
|
file |
diff |
annotate
|
2009-09-22 |
Christian Urban |
some comments
|
file |
diff |
annotate
|
2009-09-21 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-09-21 |
Christian Urban |
slight tuning
|
file |
diff |
annotate
|
2009-09-21 |
Cezary Kaliszyk |
The tactic with REPEAT, CHANGED and a proper simpset.
|
file |
diff |
annotate
|
2009-09-21 |
Cezary Kaliszyk |
Merged with my changes from the morning:
|
file |
diff |
annotate
|
2009-09-20 |
Ning |
some more beautification
|
file |
diff |
annotate
|
2009-09-20 |
Ning |
beautification of some proofs
|
file |
diff |
annotate
|
2009-09-18 |
Cezary Kaliszyk |
Added more useful quotient facts.
|
file |
diff |
annotate
|
2009-09-18 |
Cezary Kaliszyk |
Testing the tactic further.
|
file |
diff |
annotate
|
2009-09-17 |
Cezary Kaliszyk |
The tactic still only for fset
|
file |
diff |
annotate
|
2009-09-17 |
Cezary Kaliszyk |
Infrastructure for the tactic
|
file |
diff |
annotate
|
2009-09-16 |
Cezary Kaliszyk |
More naming/binding suggestions from Makarius
|
file |
diff |
annotate
|
2009-09-15 |
Cezary Kaliszyk |
Code cleanup
|
file |
diff |
annotate
|
2009-09-15 |
Cezary Kaliszyk |
Cleaning the code
|
file |
diff |
annotate
|
2009-09-15 |
Cezary Kaliszyk |
Generalized interpretation, works for all examples.
|
file |
diff |
annotate
|
2009-08-28 |
Cezary Kaliszyk |
Fixes after suggestions from Makarius:
|
file |
diff |
annotate
|
2009-08-28 |
Cezary Kaliszyk |
More examples.
|
file |
diff |
annotate
|
2009-08-27 |
Cezary Kaliszyk |
Use metavariables in the 'non-lambda' definitions
|
file |
diff |
annotate
|
2009-08-26 |
Cezary Kaliszyk |
Make both kinds of definitions.
|
file |
diff |
annotate
|
2009-08-25 |
Cezary Kaliszyk |
Changed to the use of "modern interface"
|
file |
diff |
annotate
|
2009-08-25 |
Cezary Kaliszyk |
Initial version of the function that builds goals.
|
file |
diff |
annotate
|
2009-08-25 |
Cezary Kaliszyk |
- Build an interpretation for fset from ML level and use it
|
file |
diff |
annotate
|
2009-08-24 |
Christian Urban |
added the prove command
|
file |
diff |
annotate
|
2009-08-21 |
Cezary Kaliszyk |
Fixed
|
file |
diff |
annotate
|
2009-08-21 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2009-08-20 |
cek |
UNION - Append theorem
|
file |
diff |
annotate
|
2009-08-20 |
Christian Urban |
update
|
file |
diff |
annotate
|
2009-08-18 |
Christian Urban |
updated slightly
|
file |
diff |
annotate
|
2009-08-11 |
Christian Urban |
initial commit
|
file |
diff |
annotate
|