isabelle: src/LCF/ROOT.ML@833abbc3e733 (annotated)

9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	1	(* Title: LCF/ROOT.ML
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1361 diff changeset	3	Author: Tobias Nipkow
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	val banner = "Logic for Computable Functions (in FOL)";
a5a9c433f639 Initial revision clasohm parents: diff changeset	8	writeln banner;
a5a9c433f639 Initial revision clasohm parents: diff changeset	9
121 d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 72 diff changeset	10	use_thy "LCF";