isabelle: src/CCL/ex/ROOT.ML@44b27ea94a16 (annotated)

9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	1	(* Title: CCL/ex/ROOT.ML
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	Author: Martin Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	4
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 9000 diff changeset	5	Examples for Classical Computational Logic.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	6	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	7
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 17456 diff changeset	8	use_thys ["Nat", "List", "Stream", "Flag"];