QuotMain.thy
2009-11-23 Cezary Kaliszyk domain_type in regularizing equality
2009-11-23 Cezary Kaliszyk More theorems lifted in the goal-directed way.
2009-11-23 Cezary Kaliszyk Finished temporary goal-directed lift_theorem wrapper.
2009-11-23 Christian Urban merged
2009-11-23 Christian Urban a version of inj_REPABS (needs to be looked at again later)
2009-11-23 Cezary Kaliszyk Fixes for atomize
2009-11-23 Christian Urban slight change in code layout
2009-11-23 Cezary Kaliszyk Removing dead code
2009-11-23 Cezary Kaliszyk Move atomize_goal to QuotMain
2009-11-23 Cezary Kaliszyk Moved new repabs_inj code to QuotMain
2009-11-23 Christian Urban code review with Cezary
2009-11-21 Christian Urban a little tuning of comments
2009-11-21 Christian Urban my first version of repabs injection
2009-11-21 Christian Urban tuned
2009-11-21 Christian Urban tuned
2009-11-21 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-20 Christian Urban started regularize of rtrm/qtrm version; looks quite promising
2009-11-19 Christian Urban updated to new Isabelle
2009-11-13 Christian Urban added some tracing information to all phases of lifting to the function lift_thm
2009-11-12 Cezary Kaliszyk merged
2009-11-12 Christian Urban changed the quotdata to be a symtab table (needs fixing)
2009-11-12 Christian Urban added a container for quotient constants (does not work yet though)
2009-11-11 Cezary Kaliszyk Modifications while preparing the goal-directed version.
2009-11-10 Cezary Kaliszyk More code cleaning and commenting
2009-11-09 Cezary Kaliszyk Minor cleaning and removing of some 'handle _'.
2009-11-09 Cezary Kaliszyk Cleaning and commenting
2009-11-09 Cezary Kaliszyk Fixes for the other get_fun implementation.
2009-11-06 Christian Urban updated to new Isabelle version and added a new example file
less more (0) -100 -50 -28 tip