2009-10-24 cek Undid wrong merge
2009-10-24 cek Tried rolling back
2009-10-24 cek Cleaning the mess
2009-10-24 cek Merge
2009-10-24 cek Better tactic and simplified the proof further
2009-10-23 Christian Urban fixed problem with incorrect ABS/REP name
2009-10-23 Cezary Kaliszyk Stronger tactic, simpler proof.
2009-10-23 Cezary Kaliszyk Split Finite Set example into separate file
2009-10-23 Cezary Kaliszyk eqsubst_tac
2009-10-23 Cezary Kaliszyk Trying to get a simpler lemma with the whole infrastructure
2009-10-23 Cezary Kaliszyk Using RANGE tactical allows getting rid of the quotients immediately.
2009-10-22 Cezary Kaliszyk Further developing the tactic and simplifying the proof
2009-10-22 Cezary Kaliszyk res_forall_rsp_tac further simplifies the proof
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
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
(0) +240 +1000 +3000 tip