isabelle: ROOT@1f6d79b62222 (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
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	9	chapter_definition ZF
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	Zermelo-Fraenkel set theory.
1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	12
1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	13	Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top of
1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	14	Isabelle/FOL.
75988 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
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	17	chapter_definition FOL
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	18	description "
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	19	First-Order Logic with some variations: single-sorted vs. many-sorted
1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	20	(polymorphic), classical vs. intuitionistic, domain-theory (LCF).
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	21	"
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	chapter_definition Pure
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	24	description "
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	25	The Pure logical framework.
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	26
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	27	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	28	expresses rules for Natural Deduction declaratively.
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	29	"
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	30
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	31	chapter_definition Misc
1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	32	description "Miscellaneous object-logics, tools, and experiments."
1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	33
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	34	chapter_definition Doc
ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	35	description "Sources of Documentation."

author	wenzelm
	Fri, 26 Aug 2022 23:12:42 +0200
changeset 75992	1f6d79b62222
parent 75988	ca73ced9e630
child 76000	586cad415e2f
permissions	-rw-r--r--