doc-src/IsarImplementation/Thy/logic.thy
 changeset 20451 27ea2ba48fa3 parent 20450 725a91601ed1 child 20470 c839b38a1f32
equal inserted replaced
20450:725a91601ed1 20451:27ea2ba48fa3
     3
     3
     4 theory logic imports base begin
     4 theory logic imports base begin
     5
     5
     6 chapter {* Primitive logic *}
     6 chapter {* Primitive logic *}
     7
     7
     8 section {* Syntax *}
     8 section {* Variable names *}
     9
     9
    10 subsection {* Variable names *}
    10 text FIXME

    11

    12

    13 section {* Types \label{sec:types} *}
    11
    14
    12 text {*
    15 text {*
    13   FIXME
    16   \glossary{Type class}{FIXME}

    17

    18   \glossary{Type arity}{FIXME}

    19

    20   \glossary{Sort}{FIXME}

    21

    22   FIXME classes and sorts

    23

    24

    25   \glossary{Type}{FIXME}

    26

    27   \glossary{Type constructor}{FIXME}

    28

    29   \glossary{Type variable}{FIXME}

    30

    31   FIXME simple types
    14 *}
    32 *}
    15
    33
    16
    34
    17 subsection {* Simply-typed lambda calculus *}
    35 section {* Terms \label{sec:terms} *}
    18
    36
    19 text {*
    37 text {*

    38   \glossary{Term}{FIXME}
    20
    39
    21 FIXME
    40   FIXME de-Bruijn representation of lambda terms
    22

    23 \glossary{Type}{FIXME}

    24 \glossary{Term}{FIXME}

    25

    26 *}
    41 *}
    27
    42
    46
    43
    47 text {*
    44 text {*
    48
    45
    49 FIXME
    46 FIXME
    50
    47
    53 \glossary{Type variable}{FIXME}
    50 \glossary{Type variable}{FIXME}
    54
    51
    55 *}
    52 *}
    56
    53
    57
    54
    58 section {* Theory *}
    55 section {* Theorems \label{sec:thms} *}
    59

    60 text {*

    61

    62 FIXME

    63

    64 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the

    65 theory context, but slightly more flexible since it may be used at

    66 different type-instances, due to \seeglossary{schematic

    67 polymorphism.}}

    68

    69 *}

    70

    71

    72 section {* Deduction *}

    73
    56
    74 text {*
    57 text {*
    75
    58
    76   FIXME
    59   FIXME
    77
    60
   137 subsection {* Equational reasoning *}
   120 subsection {* Equational reasoning *}
   138
   121
   139 text FIXME
   122 text FIXME
   140
   123
   141
   124
   142 section {* Proof terms *}
   125 section {* Low-level specifications *}
   143
   126
   144 text FIXME
   127 text {*

   128

   129 FIXME

   130

   131 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the

   132 theory context, but slightly more flexible since it may be used at

   133 different type-instances, due to \seeglossary{schematic

   134 polymorphism.}}

   135

   136 \glossary{Axiom}{FIXME}

   137

   138 \glossary{Primitive definition}{FIXME}

   139

   140 *}
   145
   141
   146 end
   142 end