2009-10-15 Cezary Kaliszyk A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-14 Cezary Kaliszyk Proving the proper RepAbs version
2009-10-14 Cezary Kaliszyk Forgot to save, second part of the commit
2009-10-14 Cezary Kaliszyk Manually regularized list_induct2
2009-10-14 Cezary Kaliszyk Fixed bug in regularise types. Now we can regularise list.induct.
2009-10-14 Cezary Kaliszyk Function for checking recursively if lifting is needed
2009-10-14 Cezary Kaliszyk Merge
2009-10-14 Cezary Kaliszyk Proper handling of non-lifted quantifiers, testing type freezing.
2009-10-13 Christian Urban slight simplification of atomize_thm
2009-10-13 Cezary Kaliszyk atomize_thm and meta_quantify.
2009-10-13 Cezary Kaliszyk Regularizing HOL all.
2009-10-13 Cezary Kaliszyk ":" is used for being in a set, "IN" means something else...
2009-10-13 Cezary Kaliszyk First (untested) version of regularize for abstractions.
2009-10-13 Christian Urban restored old version
2009-10-12 Christian Urban tuned
2009-10-12 Christian Urban slightly modified the parser
2009-10-12 Christian Urban deleted diagnostic code
2009-10-12 Christian Urban added quotient command (you need to update isar-keywords-prove.el)
2009-10-12 Christian Urban added new keyword
2009-10-12 Cezary Kaliszyk Bounded quantifier
2009-10-12 Cezary Kaliszyk The tyREL function.
2009-10-12 Christian Urban started some strange functions
2009-10-12 Cezary Kaliszyk Further with the manual proof
2009-10-09 Cezary Kaliszyk Further experiments with proving induction manually
2009-10-09 Cezary Kaliszyk Testing if I can prove the regularized version of induction manually
2009-10-08 Christian Urban exported parts of QuotMain into a separate ML-file
2009-10-06 Christian Urban consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
2009-10-06 Christian Urban simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
2009-10-06 Christian Urban renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
2009-10-06 Christian Urban tuned; nothing serious
2009-10-06 Christian Urban another improvement to unlam_def
2009-10-06 Christian Urban one further improvement to unlam_def
2009-10-05 Christian Urban simplified the unlam_def function
2009-10-05 Christian Urban added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)
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
2009-09-28 Christian Urban added name to prove
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.
(0) -60 +60 +100 +300 +1000 +3000 tip