QuotMain.thy
2009-09-29 Cezary Kaliszyk Merged
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.
less more (0) -24 tip