QuotMain.thy
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 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 Simplfied interface to repabs_injection.
2009-10-27 Cezary Kaliszyk map_append lifted automatically.
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 added equiv-thm to the quot_info
2009-10-27 Christian Urban made quotients compatiple with Nominal; updated keyword file
2009-10-27 Cezary Kaliszyk Completely cleaned Int.
2009-10-27 Cezary Kaliszyk Further reordering in Int code.
2009-10-26 Christian Urban merged
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 Cleaning and fixing.
2009-10-25 Christian Urban added code for declaring map-functions
2009-10-24 Christian Urban added data-storage about the quotients
2009-10-24 Christian Urban changed the definitions of liftet constants to use fun_maps
2009-10-24 Christian Urban moved the map_funs setup into QuotMain
2009-10-24 cek Undid wrong merge
2009-10-24 cek Cleaning the mess
2009-10-23 Christian Urban fixed problem with incorrect ABS/REP name
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 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 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
less more (0) -100 -96 tip