2009-11-28 Cezary Kaliszyk LFex proof a bit further.
2009-11-28 Cezary Kaliszyk merge
2009-11-28 Cezary Kaliszyk Looking at repabs proof in LF.
2009-11-28 Christian Urban further proper merge
2009-11-28 Christian Urban merged
2009-11-28 Christian Urban more simplification
2009-11-28 Cezary Kaliszyk Merged and tested that all works.
2009-11-28 Cezary Kaliszyk Finished and tested the new regularize
2009-11-28 Christian Urban more tuning of the repabs-tactics
2009-11-28 Christian Urban fixed examples in IntEx and FSet
2009-11-28 Christian Urban merged
2009-11-28 Christian Urban fixed previous commit
2009-11-28 Cezary Kaliszyk Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28 Cezary Kaliszyk Merged comment
2009-11-28 Cezary Kaliszyk Integrated Stefan's tactic and changed substs to simps with empty context.
2009-11-28 Christian Urban some slight tuning of the apply-tactic
2009-11-28 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-27 Cezary Kaliszyk Merge
2009-11-27 Cezary Kaliszyk The magical code from Stefan, will need to be integrated in the Simproc.
2009-11-27 Christian Urban replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cezary Kaliszyk Cleaning of LFex. Lambda_prs fails to unify in 2 places.
2009-11-27 Cezary Kaliszyk Recommit
2009-11-27 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27 Cezary Kaliszyk More cleaning in QuotMain, identity handling.
2009-11-27 Cezary Kaliszyk Minor cleaning
2009-11-27 Christian Urban tuned
2009-11-27 Christian Urban some tuning
2009-11-27 Christian Urban simplified gen_frees_tac and properly named abstracted variables
2009-11-27 Christian Urban removed CHANGED'
2009-11-27 Christian Urban introduced a separate lemma for id_simps
2009-11-27 Christian Urban renamed inj_REPABS to inj_repabs_trm
2009-11-27 Christian Urban tuned comments and moved slightly some code
2009-11-27 Christian Urban deleted obsolete qenv code
2009-11-27 Christian Urban renamed REGULARIZE to be regularize
2009-11-26 Christian Urban more tuning
2009-11-26 Christian Urban deleted get_fun_old and stuff
2009-11-26 Christian Urban recommited changes of comments
2009-11-26 Cezary Kaliszyk Merge Again
2009-11-26 Cezary Kaliszyk Merged
2009-11-26 Christian Urban tuned comments
2009-11-26 Christian Urban some diagnostic code for r_mk_comb
2009-11-26 Christian Urban introduced a new property for Ball and ===> on the left
2009-11-26 Christian Urban fixed QuotList
2009-11-26 Christian Urban changed left-res
2009-11-26 Cezary Kaliszyk Manually regularized akind_aty_atrm.induct
2009-11-26 Cezary Kaliszyk Playing with Monos in LFex.
2009-11-26 Cezary Kaliszyk Fixed FSet after merge.
2009-11-26 Christian Urban merged
2009-11-26 Christian Urban test with monos
2009-11-25 Cezary Kaliszyk applic_prs
2009-11-25 Christian Urban polishing
2009-11-25 Christian Urban reordered the code
2009-11-25 Cezary Kaliszyk Moved exception handling to QuotMain and cleaned FSet.
2009-11-25 Cezary Kaliszyk Merge
2009-11-25 Cezary Kaliszyk Finished manual lifting of list_induct_part :)
2009-11-25 Christian Urban comments tuning and slight reordering
2009-11-25 Cezary Kaliszyk Merge
2009-11-25 Cezary Kaliszyk More moving from QuotMain to UnusedQuotMain
2009-11-25 Christian Urban deleted some obsolete diagnostic code
2009-11-25 Cezary Kaliszyk Removed unused things from QuotMain.
2009-11-25 Cezary Kaliszyk All examples work again.
2009-11-25 Cezary Kaliszyk cleaning in MyInt
2009-11-25 Cezary Kaliszyk lambda_prs and cleaning the existing examples.
2009-11-25 Christian Urban merged
2009-11-25 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-24 Cezary Kaliszyk Ho-matching failures...
2009-11-24 Christian Urban changed unification to matching
2009-11-24 Christian Urban unification
2009-11-24 Cezary Kaliszyk Lambda & SOLVED' for new quotient_tac
2009-11-24 Christian Urban merged
2009-11-24 Cezary Kaliszyk Conversion
2009-11-24 Cezary Kaliszyk The non-working procedure_tac.
2009-11-24 Christian Urban merged
2009-11-24 Christian Urban use error instead of raising our own exception
2009-11-24 Cezary Kaliszyk Fixes to the tactic after quotient_tac changed.
2009-11-24 Christian Urban merged
2009-11-24 Christian Urban added a prepare_tac
2009-11-24 Cezary Kaliszyk TRY' for clean_tac
2009-11-24 Cezary Kaliszyk Moved cleaning to QuotMain
2009-11-24 Cezary Kaliszyk New cleaning tactic
2009-11-24 Christian Urban explicit phases for the cleaning
2009-11-24 Cezary Kaliszyk Separate regularize_tac
2009-11-24 Cezary Kaliszyk Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
2009-11-24 Cezary Kaliszyk More fixes for inj_REPABS
2009-11-24 Christian Urban addded a tactic, which sets up the three goals of the `algorithm'
2009-11-23 Christian Urban fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
2009-11-23 Christian Urban merged
2009-11-23 Christian Urban tuned some comments
2009-11-23 Cezary Kaliszyk Another not-typechecking regularized term.
2009-11-23 Cezary Kaliszyk domain_type in regularizing equality
2009-11-23 Cezary Kaliszyk More theorems lifted in the goal-directed way.
2009-11-23 Cezary Kaliszyk Finished temporary goal-directed lift_theorem wrapper.
2009-11-23 Christian Urban merged
2009-11-23 Christian Urban a version of inj_REPABS (needs to be looked at again later)
2009-11-23 Cezary Kaliszyk Fixes for atomize
2009-11-23 Cezary Kaliszyk merge
2009-11-23 Cezary Kaliszyk lift_thm with a goal.
2009-11-23 Christian Urban slight change in code layout
2009-11-23 Cezary Kaliszyk Fixes for new code
2009-11-23 Cezary Kaliszyk Removing dead code
2009-11-23 Cezary Kaliszyk Move atomize_goal to QuotMain
2009-11-23 Cezary Kaliszyk Removed second implementation of Regularize/Inject from FSet.
2009-11-23 Cezary Kaliszyk Moved new repabs_inj code to QuotMain
2009-11-23 Cezary Kaliszyk New repabs behaves the same way as old one.
2009-11-23 Christian Urban code review with Cezary
2009-11-23 Cezary Kaliszyk The other branch does not seem to work...
2009-11-23 Cezary Kaliszyk Fixes for recent changes.
2009-11-22 Christian Urban updated to Isabelle 22nd November
2009-11-21 Christian Urban a little tuning of comments
2009-11-21 Christian Urban slight tuning
2009-11-21 Christian Urban some debugging code, but cannot find the place where the cprems_of exception is raised
2009-11-21 Christian Urban tried to prove the repabs_inj lemma, but failed for the moment
2009-11-21 Christian Urban my first version of repabs injection
2009-11-21 Christian Urban tuned
2009-11-21 Christian Urban tunded
2009-11-21 Christian Urban tuned
2009-11-21 Christian Urban flagged qenv-stuff as obsolete
2009-11-21 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-20 Christian Urban started regularize of rtrm/qtrm version; looks quite promising
2009-11-19 Christian Urban updated to new Isabelle
2009-11-18 Christian Urban fixed the storage of qconst definitions
2009-11-13 Cezary Kaliszyk Still don't know how to do the proof automatically.
2009-11-13 Christian Urban added some tracing information to all phases of lifting to the function lift_thm
2009-11-12 Cezary Kaliszyk merge of the merge?
2009-11-12 Cezary Kaliszyk merged
2009-11-12 Christian Urban added a FIXME commment
2009-11-12 Christian Urban looking up data in quot_info works now (needs qualified string)
2009-11-12 Christian Urban changed the quotdata to be a symtab table (needs fixing)
2009-11-12 Christian Urban added a container for quotient constants (does not work yet though)
2009-11-11 Cezary Kaliszyk Lifting towards goal and manually finished the proof.
2009-11-11 Cezary Kaliszyk merge
2009-11-11 Cezary Kaliszyk Modifications while preparing the goal-directed version.
2009-11-11 Christian Urban updated to new Theory_Data and to new Isabelle
2009-11-11 Cezary Kaliszyk Removed 'Toplevel.program' for polyml 5.3
2009-11-10 Cezary Kaliszyk Atomizing a "goal" theorems.
2009-11-10 Cezary Kaliszyk More code cleaning and commenting
2009-11-09 Cezary Kaliszyk Minor cleaning and removing of some 'handle _'.
2009-11-09 Cezary Kaliszyk Cleaning and commenting
2009-11-09 Cezary Kaliszyk Fixes for the other get_fun implementation.
2009-11-06 Christian Urban permutation lifting works now also
2009-11-06 Christian Urban merged
2009-11-06 Christian Urban updated to new Isabelle version and added a new example file
2009-11-06 Cezary Kaliszyk Minor changes
2009-11-06 Cezary Kaliszyk merge
2009-11-06 Cezary Kaliszyk fold_rsp
2009-11-06 Christian Urban tuned the code in quotient and quotient_def
2009-11-05 Cezary Kaliszyk More functionality for lifting list.cases and list.recs.
2009-11-05 Christian Urban merged
2009-11-05 Christian Urban removed typing information from get_fun in quotient_def; *potentially* dangerous
2009-11-05 Cezary Kaliszyk Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
2009-11-05 Christian Urban removed Simplifier.context
2009-11-05 Christian Urban replaced check_term o parse_term by read_term
2009-11-05 Christian Urban merged
2009-11-05 Cezary Kaliszyk Infrastructure for polymorphic types
2009-11-04 Cezary Kaliszyk Two new tests for get_fun. Second one fails.
2009-11-04 Cezary Kaliszyk Type instantiation in regularize
2009-11-04 Cezary Kaliszyk Description of regularize
2009-11-04 Cezary Kaliszyk Experiments with lifting partially applied constants.
2009-11-04 Christian Urban more tuning
2009-11-04 Christian Urban slightly tuned
2009-11-04 Christian Urban merged
2009-11-04 Christian Urban separated the quotient_def into a separate file
2009-11-04 Cezary Kaliszyk Experiments in Int
2009-11-04 Christian Urban fixed definition of PLUS
2009-11-04 Christian Urban simplified the quotient_def code
2009-11-04 Cezary Kaliszyk Lifting 'fold1.simps(2)' and some cleaning.
2009-11-03 Cezary Kaliszyk Playing with alpha_refl.
2009-11-03 Cezary Kaliszyk Alpha.induct now lifts automatically.
2009-11-03 Cezary Kaliszyk merge
2009-11-03 Cezary Kaliszyk applic_prs
2009-11-03 Christian Urban simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
2009-11-03 Cezary Kaliszyk Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
2009-11-03 Cezary Kaliszyk merge
2009-11-03 Cezary Kaliszyk Preparing infrastructure for general FORALL_PRS
2009-11-02 Christian Urban split quotient.ML into two files
2009-11-02 Christian Urban slightly saner way of parsing the quotient_def
2009-11-02 Christian Urban merged
2009-11-02 Christian Urban changed Type.typ_match to Sign.typ_match
2009-11-02 Cezary Kaliszyk Fixes after optimization and preparing for a general FORALL_PRS
2009-11-02 Cezary Kaliszyk Optimization
2009-11-02 Cezary Kaliszyk Map does not fully work yet.
2009-11-02 Cezary Kaliszyk Fixed quotdata_lookup.
2009-11-02 Christian Urban fixed problem with maps_update
2009-11-02 Christian Urban merged
2009-11-02 Christian Urban fixed the problem with types in map
2009-10-31 Cezary Kaliszyk Automatic computation of application preservation and manually finished "alpha.induct". Slow...
2009-10-30 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts.
2009-10-30 Cezary Kaliszyk Regularization
2009-10-30 Christian Urban merged
2009-10-30 Christian Urban added some facts about fresh and support of lam
2009-10-30 Cezary Kaliszyk Finally merged the code of the versions of regularize and tested examples.
2009-10-30 Cezary Kaliszyk Lemmas about fv.
2009-10-30 Christian Urban changed the order of rfv and reformulated a3 with rfv
2009-10-30 Christian Urban merged
2009-10-30 Christian Urban not sure what changed here
2009-10-30 Christian Urban added fv-function
2009-10-30 Cezary Kaliszyk The proper real_alpha
2009-10-30 Cezary Kaliszyk Finding applications and duplicates filtered out in abstractions
2009-10-30 Cezary Kaliszyk Cleaning also in Lam
2009-10-30 Cezary Kaliszyk Cleaning of the interface to lift.
2009-10-29 Cezary Kaliszyk Tried manually lifting real_alpha
2009-10-29 Cezary Kaliszyk More tests in Lam
2009-10-29 Cezary Kaliszyk Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
2009-10-29 Cezary Kaliszyk Using subst for identity definition.
2009-10-29 Cezary Kaliszyk Lifting of the 3 lemmas in LamEx
2009-10-29 Cezary Kaliszyk Fixed wrong CARD definition and removed the "Does not work anymore" comment.
2009-10-29 Christian Urban merged
2009-10-28 Christian Urban updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
2009-10-28 Christian Urban ported all constant definitions to new scheme
2009-10-28 Christian Urban fixed the definition of alpha; this *breaks* some of the experiments
2009-10-28 Cezary Kaliszyk disambiguate ===> syntax
2009-10-28 Cezary Kaliszyk More cleaning in Lam code
2009-10-28 Cezary Kaliszyk cleaned FSet
2009-10-28 Cezary Kaliszyk Some cleaning
2009-10-28 Cezary Kaliszyk Cleaning the unnecessary theorems in 'IntEx'.
2009-10-28 Cezary Kaliszyk Fix also in the general procedure.
2009-10-28 Cezary Kaliszyk merge
2009-10-28 Cezary Kaliszyk Fixes
2009-10-28 Christian Urban updated all definitions
2009-10-28 Christian Urban merged
2009-10-28 Christian Urban added infrastructure for defining lifted constants
2009-10-28 Cezary Kaliszyk First experiments with Lambda
2009-10-28 Cezary Kaliszyk Fixed mistake in const generation, will postpone this.
2009-10-28 Cezary Kaliszyk More finshed proofs and cleaning
2009-10-28 Cezary Kaliszyk Proof of append_rsp
2009-10-28 Christian Urban merged
2009-10-28 Christian Urban added a function for matching types
2009-10-27 Cezary Kaliszyk Manual conversion of equality to equivalence allows lifting append_assoc.
2009-10-27 Cezary Kaliszyk Simplfied interface to repabs_injection.
2009-10-27 Cezary Kaliszyk map_append lifted automatically.
2009-10-27 Cezary Kaliszyk Manually lifted Map_Append.
2009-10-27 Cezary Kaliszyk Merged
2009-10-27 Cezary Kaliszyk Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
2009-10-27 Christian Urban tuned
2009-10-27 Christian Urban merged
2009-10-27 Christian Urban added equiv-thm to the quot_info
2009-10-27 Cezary Kaliszyk Simplifying FSet with new functions.
2009-10-27 Christian Urban added an example about lambda-terms
2009-10-27 Christian Urban made quotients compatiple with Nominal; updated keyword file
2009-10-27 Christian Urban merged
2009-10-27 Cezary Kaliszyk Completely cleaned Int.
2009-10-27 Cezary Kaliszyk Further reordering in Int code.
2009-10-26 Cezary Kaliszyk Simplifying Int.
2009-10-26 Cezary Kaliszyk Merge
2009-10-26 Cezary Kaliszyk Simplifying Int and Working on map
2009-10-26 Christian Urban merged
2009-10-26 Cezary Kaliszyk Simplifying code in int
2009-10-26 Cezary Kaliszyk Symmetry of integer addition
2009-10-26 Cezary Kaliszyk Finished the code for adding lower defs, and more things moved to QuotMain
2009-10-26 Cezary Kaliszyk Making all the definitions from the original ones
2009-10-26 Cezary Kaliszyk Finished COND_PRS proof.
2009-10-26 Cezary Kaliszyk Cleaning and fixing.
2009-10-26 Christian Urban updated with quotient_def
2009-10-25 Christian Urban added code for declaring map-functions
2009-10-24 Christian Urban added "print_quotients" command to th ekeyword file
2009-10-24 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall)
2009-10-24 Christian Urban added data-storage about the quotients
2009-10-24 Christian Urban added another example file about integers (see HOL/Int.thy)
2009-10-24 Christian Urban changed the definitions of liftet constants to use fun_maps
2009-10-24 cek Merge
2009-10-24 Cezary Kaliszyk Finally lifted induction, with some manually added simplification lemmas.
2009-10-24 Christian Urban changed encoding from utf8 to ISO8 (needed to work with xemacs)
2009-10-24 cek Merge
2009-10-24 Cezary Kaliszyk Preparing infrastructire for LAMBDA_PRS
2009-10-24 Christian Urban moved the map_funs setup into QuotMain
2009-10-24 Cezary Kaliszyk Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
2009-10-24 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
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) +960 +1000 tip