doc-src/IsarRef/Thy/Spec.thy
changeset 30240 5b25fee0362c
parent 29706 10e6f2faa1e5
child 30242 aea5d7fa7ef5
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -4,6 +4,24 @@
     1.4  
     1.5  chapter {* Theory specifications *}
     1.6  
     1.7 +text {*
     1.8 +  The Isabelle/Isar theory format integrates specifications and
     1.9 +  proofs, supporting interactive development with unlimited undo
    1.10 +  operation.  There is an integrated document preparation system (see
    1.11 +  \chref{ch:document-prep}), for typesetting formal developments
    1.12 +  together with informal text.  The resulting hyper-linked PDF
    1.13 +  documents can be used both for WWW presentation and printed copies.
    1.14 +
    1.15 +  The Isar proof language (see \chref{ch:proofs}) is embedded into the
    1.16 +  theory language as a proper sub-language.  Proof mode is entered by
    1.17 +  stating some @{command theorem} or @{command lemma} at the theory
    1.18 +  level, and left again with the final conclusion (e.g.\ via @{command
    1.19 +  qed}).  Some theory specification mechanisms also require a proof,
    1.20 +  such as @{command typedef} in HOL, which demands non-emptiness of
    1.21 +  the representing sets.
    1.22 +*}
    1.23 +
    1.24 +
    1.25  section {* Defining theories \label{sec:begin-thy} *}
    1.26  
    1.27  text {*
    1.28 @@ -106,9 +124,9 @@
    1.29    @{command (global) "end"} has a different meaning: it concludes the
    1.30    theory itself (\secref{sec:begin-thy}).
    1.31    
    1.32 -  \item @{text "(\<IN> c)"} given after any local theory command
    1.33 -  specifies an immediate target, e.g.\ ``@{command
    1.34 -  "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
    1.35 +  \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
    1.36 +  local theory command specifies an immediate target, e.g.\
    1.37 +  ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
    1.38    "theorem"}~@{text "(\<IN> c) \<dots>"}''.  This works both in a local or
    1.39    global theory context; the current target context will be suspended
    1.40    for this command only.  Note that ``@{text "(\<IN> -)"}'' will
    1.41 @@ -1164,7 +1182,7 @@
    1.42  
    1.43    \end{description}
    1.44  
    1.45 -  See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
    1.46 +  See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
    1.47    defining a new primitive rule as oracle, and turning it into a proof
    1.48    method.
    1.49  *}