isabelle: src/FOLP/ex/ROOT.ML@fad8634cee62 (annotated)

17480 fd19f77dcf60 converted to Isar theory format; wenzelm parents: 9000 diff changeset	1	(* Title: FOLP/ex/ROOT.ML
1459 d12da312eff4 expanded tabs clasohm parents: 1351 diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	4
17480 fd19f77dcf60 converted to Isar theory format; wenzelm parents: 9000 diff changeset	5	Examples for First-Order Logic.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	6	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	7
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 17480 diff changeset	8	use_thys [
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 17480 diff changeset	9	"Intro",
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 17480 diff changeset	10	"Nat",
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 17480 diff changeset	11	"Foundation",
26322 eaf634e975fa converted legacy ML scripts; wenzelm parents: 25991 diff changeset	12	"If",
eaf634e975fa converted legacy ML scripts; wenzelm parents: 25991 diff changeset	13	"Intuitionistic",
26408 6964c4799f47 converted legacy ML scripts; wenzelm parents: 26322 diff changeset	14	"Classical",
6964c4799f47 converted legacy ML scripts; wenzelm parents: 26322 diff changeset	15	"Propositional_Int",
6964c4799f47 converted legacy ML scripts; wenzelm parents: 26322 diff changeset	16	"Quantifiers_Int",
6964c4799f47 converted legacy ML scripts; wenzelm parents: 26322 diff changeset	17	"Propositional_Cla",
6964c4799f47 converted legacy ML scripts; wenzelm parents: 26322 diff changeset	18	"Quantifiers_Cla"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 17480 diff changeset	19	];

author	wenzelm
	Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721	fad8634cee62
parent 35762	af3ff2ba4c54
permissions	-rw-r--r--