src/HOL/Quotient_Examples/Lift_RBT.thy
Fri, 25 Nov 2011 10:52:30 +0100 bulwahn improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
Fri, 18 Nov 2011 13:50:01 +0100 bulwahn adding another example for lifting definitions
less more (0) tip