isabelle: src/HOL/Quot/ROOT.ML@0b268cff9344 (annotated)

2898 d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	1	(* Title: HOL/Quot/ROOT.ML
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	2	ID: $Id$
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	3	Author:
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	4	Copyright
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	5
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	6	Higher-order quotients.
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	7	*)
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	8
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	10
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	11	writeln"Root file for HOL/Quot";
d7bff1252d1e Higher-order quotients. wenzelm parents: diff changeset	12
2908 b9ba893e72cd Start Example slotosch parents: 2899 diff changeset	13	use_thy "FRACT";
2899 c0abd2fd9b7c * empty log message * wenzelm parents: 2898 diff changeset	14