isabelle: src/FOLP/ROOT.ML@1ebc6b76e5ff (annotated)

17480 fd19f77dcf60 converted to Isar theory format; wenzelm parents: 6349 diff changeset	1	(* Title: FOLP/ROOT.ML
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 25750 diff changeset	2	Author: Martin Coen, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	4
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	Modifed version of Lawrence Paulson's FOL that contains proof terms.
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	Presence of unknown proof term means that matching does not behave as expected.
a5a9c433f639 Initial revision clasohm parents: diff changeset	8	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	9
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 25750 diff changeset	10	use_thys ["FOLP"];
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	11