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