QuotMain.thy
2009-10-05 Christian Urban used prop_of to get the term of a theorem (replaces crep_thm)
2009-10-02 Cezary Kaliszyk Merged
2009-10-02 Cezary Kaliszyk First theorem with quantifiers. Learned how to use sledgehammer.
2009-10-01 Christian Urban simplified the storage of the map-functions by using TheoryDataFun
2009-09-30 Cezary Kaliszyk Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
2009-09-29 Christian Urban used new cong_tac
2009-09-29 Cezary Kaliszyk First version of handling of the universal quantifier
2009-09-29 Cezary Kaliszyk Handling abstraction correctly.
2009-09-29 Cezary Kaliszyk second test
2009-09-29 Cezary Kaliszyk Test line
2009-09-29 Cezary Kaliszyk Partially fix lifting of card_suc. The quantified variable still needs to be changed.
2009-09-29 Cezary Kaliszyk Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
2009-09-29 Cezary Kaliszyk Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
2009-09-29 Cezary Kaliszyk Merged
less more (0) -14 tip