2009-10-22 Cezary Kaliszyk Working on the proof and the tactic.
2009-10-22 Cezary Kaliszyk The proof gets simplified
2009-10-22 Cezary Kaliszyk Removed an assumption
2009-10-22 Cezary Kaliszyk The proof now including manually unfolded higher-order RES_FORALL_RSP.
2009-10-22 Cezary Kaliszyk The problems with 'abs' term.
2009-10-22 Cezary Kaliszyk Simplified the proof with some tactic... Still hangs sometimes.
2009-10-22 Cezary Kaliszyk More proof
2009-10-22 Cezary Kaliszyk Got rid of instantiations in the proof
2009-10-22 Cezary Kaliszyk Removed some debugging messages
2009-10-21 Christian Urban tuned and attempted to store data about the quotients (does not work yet)
2009-10-21 Christian Urban tuned
2009-10-21 Christian Urban slight tuning
2009-10-21 Christian Urban fixed my_reg
2009-10-21 Cezary Kaliszyk Reorganization of the construction part
2009-10-21 Cezary Kaliszyk Simplified proof more
2009-10-21 Cezary Kaliszyk Cleaning the code
2009-10-21 Cezary Kaliszyk Further reorganization
2009-10-21 Cezary Kaliszyk Further reorganizing the file
2009-10-21 Cezary Kaliszyk Reordering
2009-10-21 Cezary Kaliszyk cterm_instantiate also fails for some strange reason...
2009-10-21 Cezary Kaliszyk preparing arguments for res_inst_tac
2009-10-21 Cezary Kaliszyk Trying res_inst_tac
2009-10-20 Christian Urban started to write code for storing data about the quotients
2009-10-20 Christian Urban some minor tuning
2009-10-20 Christian Urban tuned and fixed the earlier fix
2009-10-20 Christian Urban fixed the abs case in my_reg and added an app case
2009-10-19 Christian Urban my version of regularise (still needs to be completed)
2009-10-19 Christian Urban moved the map-info and fun-info section to quotient.ML
2009-10-18 Cezary Kaliszyk Test if we can already do sth with the transformed theorem.
2009-10-18 Christian Urban slight fix and tuning
2009-10-17 Christian Urban the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
2009-10-17 Cezary Kaliszyk Partial simplification of the proof
2009-10-17 Cezary Kaliszyk Some QUOTIENTS
2009-10-17 Cezary Kaliszyk Only QUOTIENSs are left to fnish proof
2009-10-17 Cezary Kaliszyk More higher order unification problems
2009-10-17 Cezary Kaliszyk Merged
2009-10-17 Cezary Kaliszyk Simplified
2009-10-17 Cezary Kaliszyk Further in the proof
2009-10-17 Cezary Kaliszyk compose_tac works with the full instantiation.
2009-10-17 Christian Urban slightly simplified get_fun function
2009-10-17 Cezary Kaliszyk The instantiated version is the same modulo beta
2009-10-17 Cezary Kaliszyk Fully manually instantiated. Still fails...
2009-10-17 Cezary Kaliszyk Little progress with match/instantiate
2009-10-16 Cezary Kaliszyk Fighting with the instantiation
2009-10-16 Cezary Kaliszyk Symmetric version of REP_ABS_RSP
2009-10-16 Cezary Kaliszyk Progressing with the proof
2009-10-16 Cezary Kaliszyk Finally fix get_fun.
2009-10-16 Cezary Kaliszyk A fix for one fun_map; doesn't work for more.
2009-10-16 Christian Urban fixed the problem with function types; but only type_of works; cterm_of does not work
2009-10-15 Cezary Kaliszyk Description of the problem with get_fun.
2009-10-15 Cezary Kaliszyk A proper build_goal_term function.
2009-10-15 Cezary Kaliszyk Cleaning the code
2009-10-15 Cezary Kaliszyk Merged
2009-10-15 Cezary Kaliszyk Cleaning the proofs
2009-10-15 Cezary Kaliszyk Cleaning the code, part 4
2009-10-15 Christian Urban slightly improved tyRel
2009-10-15 Cezary Kaliszyk Reordering the code, part 3
2009-10-15 Cezary Kaliszyk Reordering the code, part 2.
2009-10-15 Cezary Kaliszyk Reordering the code, part 1.
2009-10-15 Cezary Kaliszyk Minor cleaning.
2009-10-15 Cezary Kaliszyk The definition of Fold1
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
(0) -112 +112 +1000 +3000 tip