isabelle: src/HOL/Quotient_Examples/ROOT.ML@c05e8209a3aa (annotated)

35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	(* Title: HOL/Quotient_Examples/ROOT.ML
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	Author: Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4	Testing the quotient package.
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	*)
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
45577 33b964e117bd adding another example for lifting definitions bulwahn parents: 45536 diff changeset	7	use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
33b964e117bd adding another example for lifting definitions bulwahn parents: 45536 diff changeset	8	"List_Quotient_Cset", "Lift_Set", "Lift_RBT"];
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9