misc tuning;
authorwenzelm
Thu May 08 22:05:15 2008 +0200 (2008-05-08)
changeset 26852a31203f58b20
parent 26851 0242c9c980df
child 26853 52cb0e965041
misc tuning;
doc-src/IsarRef/Thy/HOLCF_Specific.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/ML_Tactic.thy
doc-src/IsarRef/Thy/Quick_Reference.thy
doc-src/IsarRef/Thy/ZF_Specific.thy
doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/ML_Tactic.tex
doc-src/IsarRef/Thy/document/Quick_Reference.tex
doc-src/IsarRef/Thy/document/ZF_Specific.tex
doc-src/IsarRef/Thy/document/intro.tex
doc-src/IsarRef/Thy/document/pure.tex
doc-src/IsarRef/Thy/intro.thy
doc-src/IsarRef/Thy/pure.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu May 08 14:52:07 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Thu May 08 22:05:15 2008 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  imports HOLCF
     1.5  begin
     1.6  
     1.7 -chapter {* HOLCF specific elements *}
     1.8 +chapter {* Isabelle/HOLCF \label{ch:holcf} *}
     1.9  
    1.10  section {* Mixfix syntax for continuous operations *}
    1.11  
     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 14:52:07 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 22:05:15 2008 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -chapter {* HOL specific elements \label{ch:logics} *}
     2.8 +chapter {* Isabelle/HOL \label{ch:hol} *}
     2.9  
    2.10  section {* Primitive types \label{sec:hol-typedef} *}
    2.11  
    2.12 @@ -151,7 +151,7 @@
    2.13    the literature.  The more part of a record scheme may be
    2.14    instantiated by zero or more further components.  For example, the
    2.15    previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
    2.16 -  c, \<dots> = m'"}, where @{text m'} refers to a different more part.
    2.17 +  c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.
    2.18    Fixed records are special instances of record schemes, where
    2.19    ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
    2.20    element.  In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
    2.21 @@ -165,8 +165,8 @@
    2.22    \item the more part is internalized, as a free term or type
    2.23    variable,
    2.24  
    2.25 -  \item field names are externalized, they cannot be accessed within the logic
    2.26 -  as first-class values.
    2.27 +  \item field names are externalized, they cannot be accessed within
    2.28 +  the logic as first-class values.
    2.29  
    2.30    \end{enumerate}
    2.31  
    2.32 @@ -243,8 +243,8 @@
    2.33    any field (including ``@{text more}''):
    2.34  
    2.35    \begin{matharray}{lll}
    2.36 -    @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
    2.37 -    @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
    2.38 +    @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
    2.39 +    @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
    2.40    \end{matharray}
    2.41  
    2.42    There is special syntax for application of updates: @{text "r\<lparr>x :=
    2.43 @@ -262,7 +262,7 @@
    2.44    constructor function:
    2.45  
    2.46    \begin{matharray}{lll}
    2.47 -    @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\
    2.48 +    @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
    2.49    \end{matharray}
    2.50  
    2.51    \medskip We now reconsider the case of non-root records, which are
    2.52 @@ -275,29 +275,32 @@
    2.53    fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
    2.54    the above record operations will get the following types:
    2.55  
    2.56 -  \begin{matharray}{lll}
    2.57 -    @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
    2.58 +  \medskip
    2.59 +  \begin{tabular}{lll}
    2.60 +    @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
    2.61      @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> 
    2.62 -      \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
    2.63 -      \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
    2.64 -    @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> 
    2.65 -      \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\
    2.66 -  \end{matharray}
    2.67 -  \noindent
    2.68 +      \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
    2.69 +      \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
    2.70 +    @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
    2.71 +      \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
    2.72 +  \end{tabular}
    2.73 +  \medskip
    2.74  
    2.75 -  \medskip Some further operations address the extension aspect of a
    2.76 +  \noindent Some further operations address the extension aspect of a
    2.77    derived record scheme specifically: @{text "t.fields"} produces a
    2.78    record fragment consisting of exactly the new fields introduced here
    2.79    (the result may serve as a more part elsewhere); @{text "t.extend"}
    2.80    takes a fixed record and adds a given more part; @{text
    2.81    "t.truncate"} restricts a record scheme to a fixed record.
    2.82  
    2.83 -  \begin{matharray}{lll}
    2.84 -    @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\
    2.85 -    @{text "t.extend"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr> \<Rightarrow>
    2.86 -      \<zeta> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
    2.87 -    @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\
    2.88 -  \end{matharray}
    2.89 +  \medskip
    2.90 +  \begin{tabular}{lll}
    2.91 +    @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
    2.92 +    @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
    2.93 +      \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
    2.94 +    @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
    2.95 +  \end{tabular}
    2.96 +  \medskip
    2.97  
    2.98    \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
    2.99    for root records.
     3.1 --- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Thu May 08 14:52:07 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Thu May 08 22:05:15 2008 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -chapter {* ML tactic expressions \label{sec:conv-tac} *}
     3.8 +chapter {* ML tactic expressions *}
     3.9  
    3.10  text {*
    3.11    Isar Proof methods closely resemble traditional tactics, when used
     4.1 --- a/doc-src/IsarRef/Thy/Quick_Reference.thy	Thu May 08 14:52:07 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Quick_Reference.thy	Thu May 08 22:05:15 2008 +0200
     4.3 @@ -20,65 +20,78 @@
     4.4      @{command "using"}~@{text a} & indicate use of additional facts \\
     4.5      @{command "unfolding"}~@{text a} & unfold definitional equations \\
     4.6      @{command "proof"}~@{text "m\<^sub>1"}~\dots~@{command "qed"}~@{text "m\<^sub>2"} & indicate proof structure and refinements \\
     4.7 -    @{command "{"}~\dots~@{command "}"} & indicate explicit blocks \\
     4.8 +    @{command "{"}~@{text "\<dots>"}~@{command "}"} & indicate explicit blocks \\
     4.9      @{command "next"} & switch blocks \\
    4.10      @{command "note"}~@{text "a = b"} & reconsider facts \\
    4.11      @{command "let"}~@{text "p = t"} & abbreviate terms by higher-order matching \\
    4.12    \end{tabular}
    4.13  
    4.14 -  \begin{matharray}{rcl}
    4.15 -    @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof"} \Or @{command "definition"}~\dots \Or \dots \\[1ex]
    4.16 +  \medskip
    4.17 +
    4.18 +  \begin{tabular}{rcl}
    4.19 +    @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof  |"}~~@{command "definition"}~@{text "\<dots>  |  \<dots>"} \\[1ex]
    4.20      @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
    4.21 -    & \Or & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
    4.22 +    & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
    4.23      @{text prfx} & = & @{command "apply"}~@{text method} \\
    4.24 -    & \Or & @{command "using"}~@{text "facts"} \\
    4.25 -    & \Or & @{command "unfolding"}~@{text "facts"} \\
    4.26 +    & @{text "|"} & @{command "using"}~@{text "facts"} \\
    4.27 +    & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\
    4.28      @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
    4.29 -    & \Or & @{command "next"} \\
    4.30 -    & \Or & @{command "note"}~@{text "name = facts"} \\
    4.31 -    & \Or & @{command "let"}~@{text "term = term"} \\
    4.32 -    & \Or & @{command "fix"}~@{text "var\<^sup>+"} \\
    4.33 -    & \Or & @{command "assume"}~@{text "name: props"} \\
    4.34 -    & \Or & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
    4.35 +    & @{text "|"} & @{command "next"} \\
    4.36 +    & @{text "|"} & @{command "note"}~@{text "name = facts"} \\
    4.37 +    & @{text "|"} & @{command "let"}~@{text "term = term"} \\
    4.38 +    & @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\
    4.39 +    & @{text "|"} & @{command "assume"}~@{text "name: props"} \\
    4.40 +    & @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
    4.41      @{text goal} & = & @{command "have"}~@{text "name: props proof"} \\
    4.42 -    & \Or & @{command "show"}~@{text "name: props proof"} \\
    4.43 -  \end{matharray}
    4.44 +    & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\
    4.45 +  \end{tabular}
    4.46  *}
    4.47  
    4.48  
    4.49  subsection {* Abbreviations and synonyms *}
    4.50  
    4.51  text {*
    4.52 -  \begin{matharray}{rcl}
    4.53 -    @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & \equiv & @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
    4.54 -    @{command ".."} & \equiv & @{command "by"}~@{text rule} \\
    4.55 -    @{command "."} & \equiv & @{command "by"}~@{text this} \\
    4.56 -    @{command "hence"} & \equiv & @{command "then"}~@{command "have"} \\
    4.57 -    @{command "thus"} & \equiv & @{command "then"}~@{command "show"} \\
    4.58 -    @{command "from"}~@{text a} & \equiv & @{command "note"}~@{text a}~@{command "then"} \\
    4.59 -    @{command "with"}~@{text a} & \equiv & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
    4.60 -    @{command "from"}~@{text this} & \equiv & @{command "then"} \\
    4.61 -    @{command "from"}~@{text this}~@{command "have"} & \equiv & @{command "hence"} \\
    4.62 -    @{command "from"}~@{text this}~@{command "show"} & \equiv & @{command "thus"} \\
    4.63 -  \end{matharray}
    4.64 +  \begin{tabular}{rcl}
    4.65 +    @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & @{text "\<equiv>"} &
    4.66 +      @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
    4.67 +    @{command ".."} & @{text "\<equiv>"} & @{command "by"}~@{text rule} \\
    4.68 +    @{command "."} & @{text "\<equiv>"} & @{command "by"}~@{text this} \\
    4.69 +    @{command "hence"} & @{text "\<equiv>"} & @{command "then"}~@{command "have"} \\
    4.70 +    @{command "thus"} & @{text "\<equiv>"} & @{command "then"}~@{command "show"} \\
    4.71 +    @{command "from"}~@{text a} & @{text "\<equiv>"} & @{command "note"}~@{text a}~@{command "then"} \\
    4.72 +    @{command "with"}~@{text a} & @{text "\<equiv>"} & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
    4.73 +    @{command "from"}~@{text this} & @{text "\<equiv>"} & @{command "then"} \\
    4.74 +    @{command "from"}~@{text this}~@{command "have"} & @{text "\<equiv>"} & @{command "hence"} \\
    4.75 +    @{command "from"}~@{text this}~@{command "show"} & @{text "\<equiv>"} & @{command "thus"} \\
    4.76 +  \end{tabular}
    4.77  *}
    4.78  
    4.79  
    4.80  subsection {* Derived elements *}
    4.81  
    4.82  text {*
    4.83 -  \begin{matharray}{rcl}
    4.84 -    @{command "also"}@{text "\<^sub>0"} & \approx & @{command "note"}~@{text "calculation = this"} \\
    4.85 -    @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \approx & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\
    4.86 -    @{command "finally"} & \approx & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
    4.87 -    @{command "moreover"} & \approx & @{command "note"}~@{text "calculation = calculation this"} \\
    4.88 -    @{command "ultimately"} & \approx & @{command "moreover"}~@{command "from"}~@{text calculation} \\[0.5ex]
    4.89 -    @{command "presume"}~@{text "a: \<phi>"} & \approx & @{command "assume"}~@{text "a: \<phi>"} \\
    4.90 -    @{command "def"}~@{text "a: x \<equiv> t"} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "a: x \<equiv> t"} \\
    4.91 -    @{command "obtain"}~@{text "x \<WHERE> a: \<phi>"} & \approx & \dots~@{command "fix"}~@{text x}~@{command "assume"}~@{text "a: \<phi>"} \\
    4.92 -    @{command "case"}~@{text c} & \approx & @{command "fix"}~@{text x}~@{command "assume"}~@{text "c: \<phi>"} \\
    4.93 -    @{command "sorry"} & \approx & @{command "by"}~@{text cheating} \\
    4.94 -  \end{matharray}
    4.95 +  \begin{tabular}{rcl}
    4.96 +    @{command "also"}@{text "\<^sub>0"} & @{text "\<approx>"} &
    4.97 +      @{command "note"}~@{text "calculation = this"} \\
    4.98 +    @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & @{text "\<approx>"} &
    4.99 +      @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\
   4.100 +    @{command "finally"} & @{text "\<approx>"} &
   4.101 +      @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
   4.102 +    @{command "moreover"} & @{text "\<approx>"} &
   4.103 +      @{command "note"}~@{text "calculation = calculation this"} \\
   4.104 +    @{command "ultimately"} & @{text "\<approx>"} &
   4.105 +      @{command "moreover"}~@{command "from"}~@{text calculation} \\[0.5ex]
   4.106 +    @{command "presume"}~@{text "a: \<phi>"} & @{text "\<approx>"} &
   4.107 +      @{command "assume"}~@{text "a: \<phi>"} \\
   4.108 +    @{command "def"}~@{text "a: x \<equiv> t"} & @{text "\<approx>"} &
   4.109 +      @{command "fix"}~@{text x}~@{command "assume"}~@{text "a: x \<equiv> t"} \\
   4.110 +    @{command "obtain"}~@{text "x \<WHERE> a: \<phi>"} & @{text "\<approx>"} &
   4.111 +      @{text "\<dots>"}~@{command "fix"}~@{text x}~@{command "assume"}~@{text "a: \<phi>"} \\
   4.112 +    @{command "case"}~@{text c} & @{text "\<approx>"} &
   4.113 +      @{command "fix"}~@{text x}~@{command "assume"}~@{text "c: \<phi>"} \\
   4.114 +    @{command "sorry"} & @{text "\<approx>"} &
   4.115 +      @{command "by"}~@{text cheating} \\
   4.116 +  \end{tabular}
   4.117  *}
   4.118  
   4.119  
     5.1 --- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 08 14:52:07 2008 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 08 22:05:15 2008 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  imports ZF
     5.5  begin
     5.6  
     5.7 -chapter {* ZF specific elements *}
     5.8 +chapter {* Isabelle/ZF \label{ch:zf} *}
     5.9  
    5.10  section {* Type checking *}
    5.11  
     6.1 --- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu May 08 14:52:07 2008 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Thu May 08 22:05:15 2008 +0200
     6.3 @@ -20,7 +20,7 @@
     6.4  %
     6.5  \endisadelimtheory
     6.6  %
     6.7 -\isamarkupchapter{HOLCF specific elements%
     6.8 +\isamarkupchapter{Isabelle/HOLCF \label{ch:holcf}%
     6.9  }
    6.10  \isamarkuptrue%
    6.11  %
     7.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 14:52:07 2008 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 22:05:15 2008 +0200
     7.3 @@ -20,7 +20,7 @@
     7.4  %
     7.5  \endisadelimtheory
     7.6  %
     7.7 -\isamarkupchapter{HOL specific elements \label{ch:logics}%
     7.8 +\isamarkupchapter{Isabelle/HOL \label{ch:hol}%
     7.9  }
    7.10  \isamarkuptrue%
    7.11  %
    7.12 @@ -166,7 +166,7 @@
    7.13    variable, which is occasionally referred to as ``row variable'' in
    7.14    the literature.  The more part of a record scheme may be
    7.15    instantiated by zero or more further components.  For example, the
    7.16 -  previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.
    7.17 +  previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isasymrparr}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.
    7.18    Fixed records are special instances of record schemes, where
    7.19    ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}}
    7.20    element.  In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation
    7.21 @@ -180,8 +180,8 @@
    7.22    \item the more part is internalized, as a free term or type
    7.23    variable,
    7.24  
    7.25 -  \item field names are externalized, they cannot be accessed within the logic
    7.26 -  as first-class values.
    7.27 +  \item field names are externalized, they cannot be accessed within
    7.28 +  the logic as first-class values.
    7.29  
    7.30    \end{enumerate}
    7.31  
    7.32 @@ -254,8 +254,8 @@
    7.33    any field (including ``\isa{more}''):
    7.34  
    7.35    \begin{matharray}{lll}
    7.36 -    \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
    7.37 -    \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
    7.38 +    \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
    7.39 +    \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
    7.40    \end{matharray}
    7.41  
    7.42    There is special syntax for application of updates: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} abbreviates term \isa{{\isachardoublequote}x{\isacharunderscore}update\ a\ r{\isachardoublequote}}.  Further notation for
    7.43 @@ -270,7 +270,7 @@
    7.44    constructor function:
    7.45  
    7.46    \begin{matharray}{lll}
    7.47 -    \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\
    7.48 +    \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
    7.49    \end{matharray}
    7.50  
    7.51    \medskip We now reconsider the case of non-root records, which are
    7.52 @@ -283,24 +283,27 @@
    7.53    fields \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isachardoublequote}},
    7.54    the above record operations will get the following types:
    7.55  
    7.56 -  \begin{matharray}{lll}
    7.57 -    \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
    7.58 -    \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
    7.59 -    \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\
    7.60 -  \end{matharray}
    7.61 -  \noindent
    7.62 +  \medskip
    7.63 +  \begin{tabular}{lll}
    7.64 +    \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
    7.65 +    \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
    7.66 +    \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
    7.67 +  \end{tabular}
    7.68 +  \medskip
    7.69  
    7.70 -  \medskip Some further operations address the extension aspect of a
    7.71 +  \noindent Some further operations address the extension aspect of a
    7.72    derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a
    7.73    record fragment consisting of exactly the new fields introduced here
    7.74    (the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}
    7.75    takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record.
    7.76  
    7.77 -  \begin{matharray}{lll}
    7.78 -    \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\
    7.79 -    \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
    7.80 -    \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\
    7.81 -  \end{matharray}
    7.82 +  \medskip
    7.83 +  \begin{tabular}{lll}
    7.84 +    \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
    7.85 +    \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
    7.86 +    \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
    7.87 +  \end{tabular}
    7.88 +  \medskip
    7.89  
    7.90    \noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide
    7.91    for root records.%
     8.1 --- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Thu May 08 14:52:07 2008 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Thu May 08 22:05:15 2008 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4  %
     8.5  \endisadelimtheory
     8.6  %
     8.7 -\isamarkupchapter{ML tactic expressions \label{sec:conv-tac}%
     8.8 +\isamarkupchapter{ML tactic expressions%
     8.9  }
    8.10  \isamarkuptrue%
    8.11  %
     9.1 --- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Thu May 08 14:52:07 2008 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Thu May 08 22:05:15 2008 +0200
     9.3 @@ -42,29 +42,31 @@
     9.4      \mbox{\isa{\isacommand{using}}}~\isa{a} & indicate use of additional facts \\
     9.5      \mbox{\isa{\isacommand{unfolding}}}~\isa{a} & unfold definitional equations \\
     9.6      \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\dots~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & indicate proof structure and refinements \\
     9.7 -    \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\dots~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\
     9.8 +    \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\
     9.9      \mbox{\isa{\isacommand{next}}} & switch blocks \\
    9.10      \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b{\isachardoublequote}} & reconsider facts \\
    9.11      \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\ {\isacharequal}\ t{\isachardoublequote}} & abbreviate terms by higher-order matching \\
    9.12    \end{tabular}
    9.13  
    9.14 -  \begin{matharray}{rcl}
    9.15 -    \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex]
    9.16 +  \medskip
    9.17 +
    9.18 +  \begin{tabular}{rcl}
    9.19 +    \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof\ \ {\isacharbar}{\isachardoublequote}}~~\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}{\isasymdots}\ \ {\isacharbar}\ \ {\isasymdots}{\isachardoublequote}} \\[1ex]
    9.20      \isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}method\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\
    9.21 -    & \Or & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{done}}} \\[1ex]
    9.22 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{done}}} \\[1ex]
    9.23      \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\
    9.24 -    & \Or & \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
    9.25 -    & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
    9.26 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
    9.27 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
    9.28      \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\
    9.29 -    & \Or & \mbox{\isa{\isacommand{next}}} \\
    9.30 -    & \Or & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\
    9.31 -    & \Or & \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\
    9.32 -    & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\
    9.33 -    & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props{\isachardoublequote}} \\
    9.34 -    & \Or & \mbox{\isa{\isacommand{then}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\
    9.35 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{next}}} \\
    9.36 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\
    9.37 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\
    9.38 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\
    9.39 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props{\isachardoublequote}} \\
    9.40 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\
    9.41      \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
    9.42 -    & \Or & \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
    9.43 -  \end{matharray}%
    9.44 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
    9.45 +  \end{tabular}%
    9.46  \end{isamarkuptext}%
    9.47  \isamarkuptrue%
    9.48  %
    9.49 @@ -73,18 +75,19 @@
    9.50  \isamarkuptrue%
    9.51  %
    9.52  \begin{isamarkuptext}%
    9.53 -\begin{matharray}{rcl}
    9.54 -    \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
    9.55 -    \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\
    9.56 -    \mbox{\isa{\isacommand{{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{this} \\
    9.57 -    \mbox{\isa{\isacommand{hence}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\
    9.58 -    \mbox{\isa{\isacommand{thus}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\
    9.59 -    \mbox{\isa{\isacommand{from}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\
    9.60 -    \mbox{\isa{\isacommand{with}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\[1ex]
    9.61 -    \mbox{\isa{\isacommand{from}}}~\isa{this} & \equiv & \mbox{\isa{\isacommand{then}}} \\
    9.62 -    \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \equiv & \mbox{\isa{\isacommand{hence}}} \\
    9.63 -    \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \equiv & \mbox{\isa{\isacommand{thus}}} \\
    9.64 -  \end{matharray}%
    9.65 +\begin{tabular}{rcl}
    9.66 +    \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} &
    9.67 +      \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
    9.68 +    \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\
    9.69 +    \mbox{\isa{\isacommand{{\isachardot}}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{by}}}~\isa{this} \\
    9.70 +    \mbox{\isa{\isacommand{hence}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\
    9.71 +    \mbox{\isa{\isacommand{thus}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\
    9.72 +    \mbox{\isa{\isacommand{from}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\
    9.73 +    \mbox{\isa{\isacommand{with}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\[1ex]
    9.74 +    \mbox{\isa{\isacommand{from}}}~\isa{this} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}} \\
    9.75 +    \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{hence}}} \\
    9.76 +    \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{thus}}} \\
    9.77 +  \end{tabular}%
    9.78  \end{isamarkuptext}%
    9.79  \isamarkuptrue%
    9.80  %
    9.81 @@ -93,18 +96,28 @@
    9.82  \isamarkuptrue%
    9.83  %
    9.84  \begin{isamarkuptext}%
    9.85 -\begin{matharray}{rcl}
    9.86 -    \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
    9.87 -    \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\
    9.88 -    \mbox{\isa{\isacommand{finally}}} & \approx & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
    9.89 -    \mbox{\isa{\isacommand{moreover}}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
    9.90 -    \mbox{\isa{\isacommand{ultimately}}} & \approx & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
    9.91 -    \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
    9.92 -    \mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} \\
    9.93 -    \mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \approx & \dots~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
    9.94 -    \mbox{\isa{\isacommand{case}}}~\isa{c} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
    9.95 -    \mbox{\isa{\isacommand{sorry}}} & \approx & \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\
    9.96 -  \end{matharray}%
    9.97 +\begin{tabular}{rcl}
    9.98 +    \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
    9.99 +      \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
   9.100 +    \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.101 +      \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\
   9.102 +    \mbox{\isa{\isacommand{finally}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.103 +      \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
   9.104 +    \mbox{\isa{\isacommand{moreover}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.105 +      \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
   9.106 +    \mbox{\isa{\isacommand{ultimately}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.107 +      \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
   9.108 +    \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.109 +      \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
   9.110 +    \mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.111 +      \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} \\
   9.112 +    \mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.113 +      \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
   9.114 +    \mbox{\isa{\isacommand{case}}}~\isa{c} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.115 +      \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\
   9.116 +    \mbox{\isa{\isacommand{sorry}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} &
   9.117 +      \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\
   9.118 +  \end{tabular}%
   9.119  \end{isamarkuptext}%
   9.120  \isamarkuptrue%
   9.121  %
    10.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 08 14:52:07 2008 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 08 22:05:15 2008 +0200
    10.3 @@ -20,7 +20,7 @@
    10.4  %
    10.5  \endisadelimtheory
    10.6  %
    10.7 -\isamarkupchapter{ZF specific elements%
    10.8 +\isamarkupchapter{Isabelle/ZF \label{ch:zf}%
    10.9  }
   10.10  \isamarkuptrue%
   10.11  %
    11.1 --- a/doc-src/IsarRef/Thy/document/intro.tex	Thu May 08 14:52:07 2008 +0200
    11.2 +++ b/doc-src/IsarRef/Thy/document/intro.tex	Thu May 08 22:05:15 2008 +0200
    11.3 @@ -318,10 +318,8 @@
    11.4    \medskip The present text really is only a reference manual on
    11.5    Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to
    11.6    give some clues of how the concepts introduced here may be put into
    11.7 -  practice.  \Appref{ap:refcard} provides a quick reference card of
    11.8 -  the most common Isabelle/Isar language elements.  \Appref{ap:conv}
    11.9 -  offers some practical hints on converting existing Isabelle theories
   11.10 -  and proof scripts to the new format (without restructuring proofs).
   11.11 +  practice.  Especially note that \appref{ap:refcard} provides a quick
   11.12 +  reference card of the most common Isabelle/Isar language elements.
   11.13  
   11.14    Further issues concerning the Isar concepts are covered in the
   11.15    literature
    12.1 --- a/doc-src/IsarRef/Thy/document/pure.tex	Thu May 08 14:52:07 2008 +0200
    12.2 +++ b/doc-src/IsarRef/Thy/document/pure.tex	Thu May 08 22:05:15 2008 +0200
    12.3 @@ -30,8 +30,11 @@
    12.4    \Chref{ch:gen-tools} describes further Isar elements provided by
    12.5    generic tools and packages (such as the Simplifier) that are either
    12.6    part of Pure Isabelle or pre-installed in most object logics.
    12.7 -  \Chref{ch:logics} refers to object-logic specific elements (mainly
    12.8 -  for HOL and ZF).
    12.9 +  Specific language elements introduced by the major object-logics are
   12.10 +  described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
   12.11 +  (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF).  Nevertheless,
   12.12 +  examples given in the generic parts will usually refer to
   12.13 +  Isabelle/HOL as well.
   12.14  
   12.15    \medskip Isar commands may be either \emph{proper} document
   12.16    constructors, or \emph{improper commands}.  Some proof methods and
   12.17 @@ -1172,7 +1175,7 @@
   12.18  The following proof methods and attributes refer to basic logical
   12.19    operations of Isar.  Further methods and attributes are provided by
   12.20    several generic and object-logic specific tools and packages (see
   12.21 -  \chref{ch:gen-tools} and \chref{ch:logics}).
   12.22 +  \chref{ch:gen-tools} and \chref{ch:hol}).
   12.23  
   12.24    \begin{matharray}{rcl}
   12.25      \indexdef{}{method}{-}\mbox{\isa{{\isacharminus}}} & : & \isarmeth \\
    13.1 --- a/doc-src/IsarRef/Thy/intro.thy	Thu May 08 14:52:07 2008 +0200
    13.2 +++ b/doc-src/IsarRef/Thy/intro.thy	Thu May 08 22:05:15 2008 +0200
    13.3 @@ -287,10 +287,8 @@
    13.4    \medskip The present text really is only a reference manual on
    13.5    Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to
    13.6    give some clues of how the concepts introduced here may be put into
    13.7 -  practice.  \Appref{ap:refcard} provides a quick reference card of
    13.8 -  the most common Isabelle/Isar language elements.  \Appref{ap:conv}
    13.9 -  offers some practical hints on converting existing Isabelle theories
   13.10 -  and proof scripts to the new format (without restructuring proofs).
   13.11 +  practice.  Especially note that \appref{ap:refcard} provides a quick
   13.12 +  reference card of the most common Isabelle/Isar language elements.
   13.13  
   13.14    Further issues concerning the Isar concepts are covered in the
   13.15    literature
    14.1 --- a/doc-src/IsarRef/Thy/pure.thy	Thu May 08 14:52:07 2008 +0200
    14.2 +++ b/doc-src/IsarRef/Thy/pure.thy	Thu May 08 22:05:15 2008 +0200
    14.3 @@ -12,8 +12,11 @@
    14.4    \Chref{ch:gen-tools} describes further Isar elements provided by
    14.5    generic tools and packages (such as the Simplifier) that are either
    14.6    part of Pure Isabelle or pre-installed in most object logics.
    14.7 -  \Chref{ch:logics} refers to object-logic specific elements (mainly
    14.8 -  for HOL and ZF).
    14.9 +  Specific language elements introduced by the major object-logics are
   14.10 +  described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
   14.11 +  (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF).  Nevertheless,
   14.12 +  examples given in the generic parts will usually refer to
   14.13 +  Isabelle/HOL as well.
   14.14  
   14.15    \medskip Isar commands may be either \emph{proper} document
   14.16    constructors, or \emph{improper commands}.  Some proof methods and
   14.17 @@ -1172,7 +1175,7 @@
   14.18    The following proof methods and attributes refer to basic logical
   14.19    operations of Isar.  Further methods and attributes are provided by
   14.20    several generic and object-logic specific tools and packages (see
   14.21 -  \chref{ch:gen-tools} and \chref{ch:logics}).
   14.22 +  \chref{ch:gen-tools} and \chref{ch:hol}).
   14.23  
   14.24    \begin{matharray}{rcl}
   14.25      @{method_def "-"} & : & \isarmeth \\