ProgTutorial/Advanced.thy
changeset 508 633d3f013be2
parent 506 caa733190454
child 514 7e25716c3744
equal deleted inserted replaced
507:d770a7b31aeb 508:633d3f013be2
    30   other hand, store local data for a task at hand. They act like the
    30   other hand, store local data for a task at hand. They act like the
    31   ``short-term memory'' and there can be many of them that are active in
    31   ``short-term memory'' and there can be many of them that are active in
    32   parallel.
    32   parallel.
    33 *}
    33 *}
    34 
    34 
    35 section {* Theories and Setups\label{sec:theories} *}
    35 section {* Theories\label{sec:theories} *}
    36 
    36 
    37 text {*
    37 text {*
    38   Theories, as said above, are the most basic layer of abstraction in
    38   Theories, as said above, are the most basic layer of abstraction in
    39   Isabelle. They record information about definitions, syntax declarations, axioms,
    39   Isabelle. They record information about definitions, syntax declarations, axioms,
    40   theorems and much more.  For example, if a definition is made, it
    40   theorems and much more.  For example, if a definition is made, it