doc-src/IsarRef/syntax.tex
 changeset 16018 3e4e077af2e7 parent 15960 9bd6550dc004 child 16068 0e7b145c3a89
equal inserted replaced
16017:cb983795bcdf 16018:3e4e077af2e7
   434 antiquotations may involve attributes as well.  For example,
   434 antiquotations may involve attributes as well.  For example,
   435 \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
   435 \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
   436 statement where all schematic variables have been replaced by fixed ones,
   436 statement where all schematic variables have been replaced by fixed ones,
   437 which are easier to read.
   437 which are easier to read.
   438
   438
   439 \indexisarant{thm}\indexisarant{lhs}\indexisarant{rhs}\indexisarant{prop}\indexisarant{term}
   439 \indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
   440 \indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
   440 \indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}

   441 \indexisarant{term-style}\indexisarant{text}\indexisarant{goals}

   442 \indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}

   443
   441 \begin{rail}
   444 \begin{rail}
   442   atsign lbrace antiquotation rbrace
   445   atsign lbrace antiquotation rbrace
   443   ;
   446   ;
   444
   447
   445   antiquotation:
   448   antiquotation:
   514   the full proof terms, i.e.\ also displays information omitted in
   517   the full proof terms, i.e.\ also displays information omitted in
   515   the compact proof term, which is denoted by $_$'' placeholders there.
   518   the compact proof term, which is denoted by $_$'' placeholders there.
   516
   519
   517 \end{descr}
   520 \end{descr}
   518
   521
   519 Per default, each theory contains three default styles for use with
   522 There are a few standard styles for use with $\at\{thm_style~s~a\}$ and
   520 $\at\{thm_style~s~a\}$ and $\at\{term_style~s~t\}$:
   523 $\at\{term_style~s~t\}$:
   521
   524
   522 \begin{descr}
   525 \begin{descr}
   523
   526
   524 \item [$lhs$] extracts the left hand sides of terms; this style only works
   527 \item [$lhs$] extracts the first argument of any application form with at
   525     for terms that are definitions, equations or other binary operators.
   528   least two arguments -- typically is meta-level or object-level equality or
   526
   529   any other binary relation.
   527 \item [$rhs$] extracts the right hand sides of terms; likewise,
   530
   528     this style only works
   531 \item [$rhs$] similar to $lhs$, but extracts the second argument.
   529     for terms that are definitions, equations or other binary operators.
   532
   530
   533 \item [$conlusion$] extracts the conclusion $C$ from nested meta-level
   531 \item [$conlusion$] extracts the conclusion from propositions.
   534   implications $A@1 \Imp \cdots A@n \Imp C$.
   532
   535
   533 \end{descr}
   536 \end{descr}
   534
   537
   535 Further styles may be defined at ML level.
   538 Further styles may be defined at ML level.
   536
   539