isabelle: src/FOL/ROOT@efd995488228 (annotated)

51397 03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 48738 diff changeset	1	chapter FOL
03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 48738 diff changeset	2
48738 f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default; wenzelm parents: 48487 diff changeset	3	session FOL = Pure +
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	4	description "
51403 2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	5	First-Order Logic with Natural Deduction (constructive and classical
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	6	versions). For a classical sequent calculus, see Isabelle/LK.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	7
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	8	Useful references on First-Order Logic:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	9
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	10	Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	11	1991) (The first chapter is an excellent introduction to natural deduction
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	12	in general.)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	13
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	14	Antony Galton, Logic for Information Technology (Wiley, 1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	15
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	16	Michael Dummett, Elements of Intuitionism (Oxford, 1977)
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	17	"
65374 a5b38d8d3c1e tuned syntax; wenzelm parents: 61935 diff changeset	18	theories
a5b38d8d3c1e tuned syntax; wenzelm parents: 61935 diff changeset	19	IFOL (global)
a5b38d8d3c1e tuned syntax; wenzelm parents: 61935 diff changeset	20	FOL (global)
56781 f2eb0f22589f systematic replacement of 'files' by 'document_files'; wenzelm parents: 52488 diff changeset	21	document_files "root.tex"
48280 7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	22
48738 f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default; wenzelm parents: 48487 diff changeset	23	session "FOL-ex" in ex = FOL +
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	24	description "
51403 2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	25	Examples for First-Order Logic.
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	26	"
70675 efd995488228 declare session directories; wenzelm parents: 69319 diff changeset	27	directories "Locale_Test"
48280 7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	28	theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	29	Natural_Numbers
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	30	Intro
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	31	Nat
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	32	Nat_Class
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	33	Foundation
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	34	Prolog
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	35	Intuitionistic
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	36	Propositional_Int
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	37	Quantifiers_Int
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	38	Classical
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	39	Propositional_Cla
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	40	Quantifiers_Cla
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	41	Miniscope
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF; wenzelm parents: diff changeset	42	If
51558 91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example; wenzelm parents: 51403 diff changeset	43	theories [document = false, skip_proofs = false]
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example; wenzelm parents: 51403 diff changeset	44	"Locale_Test/Locale_Test"
56781 f2eb0f22589f systematic replacement of 'files' by 'document_files'; wenzelm parents: 52488 diff changeset	45	document_files "root.tex"

author	wenzelm
	Sun, 08 Sep 2019 16:49:05 +0200
changeset 70675	efd995488228
parent 69319	baccaf89ca0d
permissions	-rw-r--r--