doc-src/IsarImplementation/Thy/Isar.thy
author wenzelm
Mon Feb 16 21:23:34 2009 +0100 (2009-02-16)
changeset 29759 bcb79ddf57da
parent 29755 d66b34e46bdf
child 30270 61811c9224a6
permissions -rw-r--r--
removed rudiments of glossary;
tuned outline;
wenzelm@29755
     1
theory Isar
wenzelm@29755
     2
imports Base
wenzelm@29755
     3
begin
wenzelm@20472
     4
wenzelm@29759
     5
chapter {* Isar language elements *}
wenzelm@29759
     6
wenzelm@29759
     7
text {*
wenzelm@29759
     8
  The primary Isar language consists of three main categories of
wenzelm@29759
     9
  language elements:
wenzelm@29759
    10
wenzelm@29759
    11
  \begin{enumerate}
wenzelm@29759
    12
wenzelm@29759
    13
  \item Proof commands
wenzelm@20472
    14
wenzelm@29759
    15
  \item Proof methods
wenzelm@29759
    16
wenzelm@29759
    17
  \item Attributes
wenzelm@29759
    18
wenzelm@29759
    19
  \end{enumerate}
wenzelm@29759
    20
*}
wenzelm@29759
    21
wenzelm@29759
    22
wenzelm@29759
    23
section {* Proof commands *}
wenzelm@20520
    24
wenzelm@20520
    25
text FIXME
wenzelm@20520
    26
wenzelm@20520
    27
wenzelm@20472
    28
section {* Proof methods *}
wenzelm@20472
    29
wenzelm@20472
    30
text FIXME
wenzelm@20472
    31
wenzelm@29759
    32
wenzelm@20472
    33
section {* Attributes *}
wenzelm@20472
    34
wenzelm@29759
    35
text FIXME
wenzelm@20472
    36
wenzelm@20472
    37
end