QuotMain.thy
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
less more (0) -100 -60 tip