isabelle: src/Cube/ROOT.ML@d8efc2490b8e (annotated)

3511 da4dd8b7ced4 removed obsolete init_pps and init_thy_reader; wenzelm parents: 2237 diff changeset	1	(* Title: Cube/ROOT.ML
1459 d12da312eff4 expanded tabs clasohm parents: 1361 diff changeset	2	Author: Tobias Nipkow
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	4
3511 da4dd8b7ced4 removed obsolete init_pps and init_thy_reader; wenzelm parents: 2237 diff changeset	5	The Lambda-Cube a la Barendregt.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	6	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	7
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 17453 diff changeset	8	use_thys ["Cube", "Example"];