isabelle: src/HOL/Quotient_Examples/Lift_RBT.thy@caaa1a02c650 (annotated)

47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47097 diff changeset	1	(* Title: HOL/Quotient_Examples/Lift_RBT.thy
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47097 diff changeset	2	Author: Lukas Bulwahn and Ondrej Kuncar
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47097 diff changeset	3	*)
45577 33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	4
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	5	header {* Lifting operations of RBT trees *}
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	6
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	7	theory Lift_RBT
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	8	imports Main "~~/src/HOL/Library/RBT_Impl"
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	9	begin
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	10
48622 caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT kuncar parents: 48621 diff changeset	11	(* Moved to ~~/HOL/Library/RBT" *)
45577 33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	12
33b964e117bd adding another example for lifting definitions bulwahn parents: diff changeset	13	end

author	kuncar
	Tue, 31 Jul 2012 13:55:39 +0200
changeset 48622	caaa1a02c650
parent 48621	877df57629e3
permissions	-rw-r--r--