isabelle: src/HOL/Quotient_Examples/ROOT.ML@c4f5823f282d (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
36280 c4f5823f282d Finite set theory Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35222 diff changeset	7	use_thys ["FSet", "LarryInt", "LarryDatatype"];
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Fri, 23 Apr 2010 10:00:53 +0200
changeset 36280	c4f5823f282d
parent 35222	4f1fba00f66d
child 36524	3909002beca5
permissions	-rw-r--r--