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