isabelle: ROOT@b4f892d0625d (annotated)

75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	1	chapter_definition HOL
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	2	description "
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	3	Higher-Order Logic.
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	4
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	5	Isabelle/HOL is a version of classical higher-order logic resembling
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	6	that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL).
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	7	"
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	8
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	9	chapter_definition FOL
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	10	description "
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	11	First-Order Logic with some variations: single-sorted vs. many-sorted
76006 c9d56340b56e ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website); wenzelm parents: 76004 diff changeset	12	(polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs.
c9d56340b56e ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website); wenzelm parents: 76004 diff changeset	13	set-theory (ZF).
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	14	"
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	15
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	16	chapter_definition Pure
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	17	description "
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	18	The Pure logical framework.
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	19
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	20	Isabelle/Pure is a version of intuitionistic higher-order logic that
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	21	expresses rules for Natural Deduction declaratively.
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	22	"
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	23
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	24	chapter_definition Misc
76000 586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	25	description "
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	26	Miscellaneous object-logics, tools, and experiments.
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	27	"
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	28
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	29	chapter_definition Doc
76000 586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	30	description "
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	31	Sources of Documentation.
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	32	"
76004 152c5c83c119 proper chapter_definition to prevent odd definitions by users; wenzelm parents: 76000 diff changeset	33
152c5c83c119 proper chapter_definition to prevent odd definitions by users; wenzelm parents: 76000 diff changeset	34	chapter_definition Unsorted
152c5c83c119 proper chapter_definition to prevent odd definitions by users; wenzelm parents: 76000 diff changeset	35	description "
152c5c83c119 proper chapter_definition to prevent odd definitions by users; wenzelm parents: 76000 diff changeset	36	Sessions without 'chapter' declaration.
152c5c83c119 proper chapter_definition to prevent odd definitions by users; wenzelm parents: 76000 diff changeset	37	"

author	paulson <lp15@cam.ac.uk>
	Wed, 25 Jan 2023 13:37:44 +0000
changeset 77089	b4f892d0625d
parent 76006	c9d56340b56e
permissions	-rw-r--r--