isabelle: src/CCL/ROOT.ML@91ba394cc525 (annotated)

9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	1	(* Title: CCL/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	Classical Computational Logic based on First-Order Logic.
32740 9dd0a2f83429 explicit indication of Unsynchronized.ref; wenzelm parents: 32153 diff changeset	6
9dd0a2f83429 explicit indication of Unsynchronized.ref; wenzelm parents: 32153 diff changeset	7	A computational logic for an untyped functional language with
9dd0a2f83429 explicit indication of Unsynchronized.ref; wenzelm parents: 32153 diff changeset	8	evaluation to weak head-normal form.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	9	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
38798 89f273ab1d42 expanded some aliases from structure Unsynchronized; wenzelm parents: 32740 diff changeset	11	eta_contract := true;
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	12
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 20140 diff changeset	13	use_thys ["Wfd", "Fix"];