src/HOL/Quotient_Examples/Lift_RBT.thy
Fri, 23 Mar 2012 14:18:43 +0100 kuncar store the quotient theorem for every quotient
Fri, 23 Mar 2012 14:17:29 +0100 kuncar fix Quotient_Examples
Fri, 06 Jan 2012 10:19:49 +0100 haftmann incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
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