ROOT
author wenzelm
Mon, 05 Feb 2024 12:59:34 +0100
changeset 79578 4c4d71b00001
parent 76006 c9d56340b56e
permissions -rw-r--r--
tuned README;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
  "