isabelle: ROOT@586cad415e2f (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
76000 586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	32	description "
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	33	Miscellaneous object-logics, tools, and experiments.
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	34	"
75992 1f6d79b62222 clarified chapters: de-emphasize minor examples; wenzelm parents: 75988 diff changeset	35
75988 ca73ced9e630 provide chapter descriptions, based on lib/html/library_index_content.template; wenzelm parents: diff changeset	36	chapter_definition Doc
76000 586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	37	description "
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	38	Sources of Documentation.
586cad415e2f tuned whitespace for presentation; wenzelm parents: 75992 diff changeset	39	"

author	wenzelm
	Sat, 27 Aug 2022 15:29:02 +0200
changeset 76000	586cad415e2f
parent 75992	1f6d79b62222
child 76004	152c5c83c119
permissions	-rw-r--r--