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

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

author	wenzelm
	Tue, 06 Jan 2009 14:45:45 +0100
changeset 29369	393f72663b49
parent 26408	6964c4799f47
child 35762	af3ff2ba4c54
permissions	-rw-r--r--