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