Quot/Examples/LamEx.thy
2010-01-15 Cezary Kaliszyk Appropriate respects and a statement of the lifted hom lemma
2010-01-15 Christian Urban recursion-hom for lambda
2010-01-15 Cezary Kaliszyk Incorrect version of the homomorphism lemma
2010-01-14 Christian Urban tuned quotient_def.ML and cleaned somewhat LamEx.thy
2010-01-14 Christian Urban a few more lemmas...except supp of lambda-abstractions
2010-01-14 Christian Urban removed one sorry
2010-01-14 Christian Urban nearly all of the proof
2010-01-14 Christian Urban right generalisation
2010-01-14 Cezary Kaliszyk First subgoal.
2010-01-14 Christian Urban setup for strong induction
2010-01-14 Cezary Kaliszyk exported absrep_const for nitpick.
2010-01-14 Cezary Kaliszyk minor
2010-01-01 Christian Urban tuned
2009-12-19 Christian Urban on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
2009-12-19 Christian Urban renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
2009-12-17 Christian Urban moved the QuotMain code into two ML-files
2009-12-11 Cezary Kaliszyk New syntax for definitions.
2009-12-09 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-08 Christian Urban changed names of attributes
2009-12-07 Christian Urban removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
2009-12-07 Christian Urban added "end" to each example theory
2009-12-07 Cezary Kaliszyk List moved after QuotMain
2009-12-07 Christian Urban directory re-arrangement
less more (0) tip