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)
(0) -120 +120 +1000 tip