isabelle: src/HOL/Quotient_Examples/ROOT.ML@7a5c681c0265 (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
47660 7a5c681c0265 new example theory for quotient/transfer huffman parents: 47308 diff changeset	7	use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet",
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47232 diff changeset	8	"Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9