1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(* $Id$ *)
     1.5 -
     1.6 -theory "ML" imports base begin
     1.7 +theory "ML"
     1.8 +imports Base
     1.9 +begin
    1.10  
    1.11  chapter {* Advanced ML programming *}
    1.12  

     2.1 --- a/doc-src/IsarImplementation/Thy/ROOT.ML	Wed Mar 04 10:43:39 2009 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Wed Mar 04 10:45:52 2009 +0100
     2.3 @@ -1,11 +1,11 @@
     2.4 -
     2.5 -(* $Id$ *)
     2.6 -
     2.7 -use_thy "prelim";
     2.8 -use_thy "logic";
     2.9 -use_thy "tactic";
    2.10 -use_thy "proof";
    2.11 -use_thy "isar";
    2.12 -use_thy "locale";
    2.13 -use_thy "integration";
    2.14 -use_thy "ML";
    2.15 +use_thys [
    2.16 +  "Integration",
    2.17 +  "Isar",
    2.18 +  "Local_Theory",
    2.19 +  "Logic",
    2.20 +  "ML",
    2.21 +  "Prelim",
    2.22 +  "Proof",
    2.23 +  "Syntax",
    2.24 +  "Tactic"
    2.25 +];

     3.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Mar 04 10:43:39 2009 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Mar 04 10:45:52 2009 +0100
     3.3 @@ -3,14 +3,14 @@
     3.4  \def\isabellecontext{ML}%
     3.5  %
     3.6  \isadelimtheory
     3.7 -\isanewline
     3.8 -\isanewline
     3.9  %
    3.10  \endisadelimtheory
    3.11  %
    3.12  \isatagtheory
    3.13  \isacommand{theory}\isamarkupfalse%
    3.14 -\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    3.15 +\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
    3.16 +\isakeyword{imports}\ Base\isanewline
    3.17 +\isakeyword{begin}%
    3.18  \endisatagtheory
    3.19  {\isafoldtheory}%
    3.20  %
    3.21 @@ -275,9 +275,9 @@
    3.22  %
    3.23  \begin{isamarkuptext}%
    3.24  \begin{mldecls}
    3.25 -  \indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
    3.26 -  \indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
    3.27 -  \indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
    3.28 +  \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
    3.29 +  \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
    3.30 +  \indexdef{}{ML}{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
    3.31    \end{mldecls}
    3.32  
    3.33    \begin{description}
    3.34 @@ -331,7 +331,7 @@
    3.35  %
    3.36  \begin{isamarkuptext}%
    3.37  \begin{mldecls}
    3.38 -  \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
    3.39 +  \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
    3.40    \end{mldecls}%
    3.41  \end{isamarkuptext}%
    3.42  \isamarkuptrue%
    3.43 @@ -410,10 +410,10 @@
    3.44  %
    3.45  \begin{isamarkuptext}%
    3.46  \begin{mldecls}
    3.47 -  \indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
    3.48 -  \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
    3.49 -  \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
    3.50 -  \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
    3.51 +  \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
    3.52 +  \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
    3.53 +  \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
    3.54 +  \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
    3.55    \end{mldecls}%
    3.56  \end{isamarkuptext}%
    3.57  \isamarkuptrue%
    3.58 @@ -483,8 +483,8 @@
    3.59  %
    3.60  \begin{isamarkuptext}%
    3.61  \begin{mldecls}
    3.62 -  \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
    3.63 -  \indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
    3.64 +  \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
    3.65 +  \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
    3.66    \end{mldecls}%
    3.67  \end{isamarkuptext}%
    3.68  \isamarkuptrue%
    3.69 @@ -545,11 +545,11 @@
    3.70  %
    3.71  \begin{isamarkuptext}%
    3.72  \begin{mldecls}
    3.73 -  \indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
    3.74 -  \indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
    3.75 -  \indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
    3.76 -  \indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
    3.77 -  \indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
    3.78 +  \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
    3.79 +  \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
    3.80 +  \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
    3.81 +  \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
    3.82 +  \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
    3.83    \end{mldecls}%
    3.84  \end{isamarkuptext}%
    3.85  \isamarkuptrue%
    3.86 @@ -576,8 +576,8 @@
    3.87  %
    3.88  \begin{isamarkuptext}%
    3.89  \begin{mldecls}
    3.90 -  \indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
    3.91 -  \indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
    3.92 +  \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
    3.93 +  \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
    3.94    \end{mldecls}%
    3.95  \end{isamarkuptext}%
    3.96  \isamarkuptrue%
    3.97 @@ -619,14 +619,14 @@
    3.98  %
    3.99  \begin{isamarkuptext}%
   3.100  \begin{mldecls}
   3.101 -  \indexml{is\_some}\verb|is_some: 'a option -> bool| \\
   3.102 -  \indexml{is\_none}\verb|is_none: 'a option -> bool| \\
   3.103 -  \indexml{the}\verb|the: 'a option -> 'a| \\
   3.104 -  \indexml{these}\verb|these: 'a list option -> 'a list| \\
   3.105 -  \indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\
   3.106 -  \indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
   3.107 -  \indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
   3.108 -  \indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
   3.109 +  \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
   3.110 +  \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
   3.111 +  \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
   3.112 +  \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
   3.113 +  \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
   3.114 +  \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
   3.115 +  \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
   3.116 +  \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
   3.117    \end{mldecls}%
   3.118  \end{isamarkuptext}%
   3.119  \isamarkuptrue%
   3.120 @@ -659,10 +659,10 @@
   3.121  %
   3.122  \begin{isamarkuptext}%
   3.123  \begin{mldecls}
   3.124 -  \indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
   3.125 -  \indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
   3.126 -  \indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
   3.127 -  \indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
   3.128 +  \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
   3.129 +  \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
   3.130 +  \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
   3.131 +  \indexdef{}{ML}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
   3.132    \end{mldecls}%
   3.133  \end{isamarkuptext}%
   3.134  \isamarkuptrue%
   3.135 @@ -690,19 +690,19 @@
   3.136  %
   3.137  \begin{isamarkuptext}%
   3.138  \begin{mldecls}
   3.139 -  \indexmlexception{AList.DUP}\verb|exception AList.DUP| \\
   3.140 -  \indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
   3.141 -  \indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
   3.142 -  \indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   3.143 -  \indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   3.144 -  \indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
   3.145 -  \indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
   3.146 +  \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
   3.147 +  \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
   3.148 +  \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
   3.149 +  \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   3.150 +  \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
   3.151 +  \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
   3.152 +  \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
   3.153  \verb|    -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
   3.154 -  \indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
   3.155 +  \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
   3.156  \verb|    -> ('a * 'b) list -> ('a * 'b) list| \\
   3.157 -  \indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
   3.158 +  \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
   3.159  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
   3.160 -  \indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
   3.161 +  \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
   3.162  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
   3.163    \end{mldecls}%
   3.164  \end{isamarkuptext}%
   3.165 @@ -732,25 +732,25 @@
   3.166  %
   3.167  \begin{isamarkuptext}%
   3.168  \begin{mldecls}
   3.169 -  \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
   3.170 -  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
   3.171 -  \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
   3.172 -  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
   3.173 -  \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
   3.174 -  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
   3.175 -  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
   3.176 -  \indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
   3.177 -  \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
   3.178 -  \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
   3.179 +  \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
   3.180 +  \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
   3.181 +  \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
   3.182 +  \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
   3.183 +  \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
   3.184 +  \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
   3.185 +  \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
   3.186 +  \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
   3.187 +  \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
   3.188 +  \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
   3.189  \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
   3.190 -  \indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
   3.191 +  \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
   3.192  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   3.193 -  \indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
   3.194 +  \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
   3.195  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   3.196 -  \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
   3.197 +  \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
   3.198  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   3.199  \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
   3.200 -  \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
   3.201 +  \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
   3.202  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   3.203  \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
   3.204    \end{mldecls}%

     4.1 --- a/doc-src/IsarImplementation/Thy/document/session.tex	Wed Mar 04 10:43:39 2009 +0100
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/session.tex	Wed Mar 04 10:45:52 2009 +0100
     4.3 @@ -1,21 +1,23 @@
     4.4 -\input{base.tex}
     4.5 +\input{Base.tex}
     4.6  
     4.7 -\input{prelim.tex}
     4.8 +\input{Integration.tex}
     4.9  
    4.10 -\input{logic.tex}
    4.11 +\input{Isar.tex}
    4.12  
    4.13 -\input{tactic.tex}
    4.14 +\input{Local_Theory.tex}
    4.15  
    4.16 -\input{proof.tex}
    4.17 -
    4.18 -\input{isar.tex}
    4.19 -
    4.20 -\input{locale.tex}
    4.21 -
    4.22 -\input{integration.tex}
    4.23 +\input{Logic.tex}
    4.24  
    4.25  \input{ML.tex}
    4.26  
    4.27 +\input{Prelim.tex}
    4.28 +
    4.29 +\input{Proof.tex}
    4.30 +
    4.31 +\input{Syntax.tex}
    4.32 +
    4.33 +\input{Tactic.tex}
    4.34 +
    4.35  %%% Local Variables:
    4.36  %%% mode: latex
    4.37  %%% TeX-master: "root"

     5.1 --- a/doc-src/IsarImplementation/implementation.tex	Wed Mar 04 10:43:39 2009 +0100
     5.2 +++ b/doc-src/IsarImplementation/implementation.tex	Wed Mar 04 10:45:52 2009 +0100
     5.3 @@ -1,6 +1,3 @@
     5.4 -
     5.5 -%% $Id$
     5.6 -
     5.7  \documentclass[12pt,a4paper,fleqn]{report}
     5.8  \usepackage{latexsym,graphicx}
     5.9  \usepackage[refpage]{nomencl}
    5.10 @@ -23,9 +20,6 @@
    5.11    and Larry Paulson
    5.12  }
    5.13  
    5.14 -%FIXME
    5.15 -%\makeglossary
    5.16 -
    5.17  \makeindex
    5.18  
    5.19  
    5.20 @@ -71,28 +65,24 @@
    5.21  \listoffigures
    5.22  \clearfirst
    5.23  
    5.24 -%\input{intro.tex}
    5.25 -\input{Thy/document/prelim.tex}
    5.26 -\input{Thy/document/logic.tex}
    5.27 -\input{Thy/document/tactic.tex}
    5.28 -\input{Thy/document/proof.tex}
    5.29 -\input{Thy/document/isar.tex}
    5.30 -\input{Thy/document/locale.tex}
    5.31 -\input{Thy/document/integration.tex}
    5.32 +\input{Thy/document/Prelim.tex}
    5.33 +\input{Thy/document/Logic.tex}
    5.34 +\input{Thy/document/Tactic.tex}
    5.35 +\input{Thy/document/Proof.tex}
    5.36 +\input{Thy/document/Syntax.tex}
    5.37 +\input{Thy/document/Isar.tex}
    5.38 +\input{Thy/document/Local_Theory.tex}
    5.39 +\input{Thy/document/Integration.tex}
    5.40  
    5.41  \appendix
    5.42  \input{Thy/document/ML.tex}
    5.43  
    5.44  \begingroup
    5.45  \tocentry{\bibname}
    5.46 -\bibliographystyle{plain} \small\raggedright\frenchspacing
    5.47 +\bibliographystyle{abbrv} \small\raggedright\frenchspacing
    5.48  \bibliography{../manual}
    5.49  \endgroup
    5.50  
    5.51 -%FIXME
    5.52 -%\tocentry{\glossaryname}
    5.53 -%\printglossary
    5.54 -
    5.55  \tocentry{\indexname}
    5.56  \printindex
    5.57  

     6.1 --- a/doc-src/IsarImplementation/style.sty	Wed Mar 04 10:43:39 2009 +0100
     6.2 +++ b/doc-src/IsarImplementation/style.sty	Wed Mar 04 10:45:52 2009 +0100
     6.3 @@ -1,6 +1,3 @@
     6.4 -
     6.5 -%% $Id$
     6.6 -
     6.7  %% toc
     6.8  \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     6.9  \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
    6.10 @@ -10,24 +7,12 @@
    6.11  \newcommand{\chref}[1]{chapter~\ref{#1}}
    6.12  \newcommand{\figref}[1]{figure~\ref{#1}}
    6.13  
    6.14 -%% glossary
    6.15 -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
    6.16 -\newcommand{\seeglossary}[1]{\emph{#1}}
    6.17 -\newcommand{\glossaryname}{Glossary}
    6.18 -\renewcommand{\nomname}{\glossaryname}
    6.19 -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
    6.20 -
    6.21 -%% index
    6.22 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    6.23 -\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
    6.24 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    6.25 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    6.26 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    6.27 -
    6.28  %% math
    6.29  \newcommand{\text}[1]{\mbox{#1}}
    6.30  \newcommand{\isasymvartheta}{\isamath{\theta}}
    6.31 -\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    6.32 +\newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
    6.33 +\newcommand{\isactrlBG}{\isacharbackquoteopen}
    6.34 +\newcommand{\isactrlEN}{\isacharbackquoteclose}
    6.35  
    6.36  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    6.37  
    6.38 @@ -49,6 +34,10 @@
    6.39  \newcommand{\isasymtype}{\minorcmd{type}}
    6.40  \newcommand{\isasymval}{\minorcmd{val}}
    6.41  
    6.42 +\newcommand{\isasymFIX}{\isakeyword{fix}}
    6.43 +\newcommand{\isasymASSUME}{\isakeyword{assume}}
    6.44 +\newcommand{\isasymDEFINE}{\isakeyword{define}}
    6.45 +\newcommand{\isasymNOTE}{\isakeyword{note}}
    6.46  \newcommand{\isasymGUESS}{\isakeyword{guess}}
    6.47  \newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    6.48  \newcommand{\isasymTHEORY}{\isakeyword{theory}}
    6.49 @@ -61,6 +50,7 @@
    6.50  
    6.51  \isabellestyle{it}
    6.52  
    6.53 +
    6.54  %%% Local Variables: 
    6.55  %%% mode: latex
    6.56  %%% TeX-master: "implementation"

     7.1 --- a/doc-src/IsarRef/IsaMakefile	Wed Mar 04 10:43:39 2009 +0100
     7.2 +++ b/doc-src/IsarRef/IsaMakefile	Wed Mar 04 10:45:52 2009 +0100
     7.3 @@ -22,10 +22,11 @@
     7.4  HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
     7.5  
     7.6  $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
     7.7 -  Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy	\
     7.8 -  Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy	\
     7.9 -  Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy		\
    7.10 -  Thy/Symbols.thy Thy/ML_Tactic.thy
    7.11 +  Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy	\
    7.12 +  Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy	\
    7.13 +  Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy		\
    7.14 +  Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Symbols.thy		\
    7.15 +  Thy/ML_Tactic.thy
    7.16  	@$(USEDIR) -s IsarRef HOL Thy
    7.17  
    7.18  

     8.1 --- a/doc-src/IsarRef/Makefile	Wed Mar 04 10:43:39 2009 +0100
     8.2 +++ b/doc-src/IsarRef/Makefile	Wed Mar 04 10:45:52 2009 +0100
     8.3 @@ -1,7 +1,3 @@
     8.4 -#
     8.5 -# $Id$
     8.6 -#
     8.7 -
     8.8  ## targets
     8.9  
    8.10  default: dvi

     9.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Wed Mar 04 10:43:39 2009 +0100
     9.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Wed Mar 04 10:45:52 2009 +0100
     9.3 @@ -1,5 +1,3 @@
     9.4 -(* $Id$ *)
     9.5 -
     9.6  theory Document_Preparation
     9.7  imports Main
     9.8  begin

    10.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Wed Mar 04 10:43:39 2009 +0100
    10.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Wed Mar 04 10:45:52 2009 +0100
    10.3 @@ -1,5 +1,3 @@
    10.4 -(* $Id$ *)
    10.5 -
    10.6  theory Generic
    10.7  imports Main
    10.8  begin

    11.1 --- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed Mar 04 10:43:39 2009 +0100
    11.2 +++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed Mar 04 10:45:52 2009 +0100
    11.3 @@ -1,5 +1,3 @@
    11.4 -(* $Id$ *)
    11.5 -
    11.6  theory HOLCF_Specific
    11.7  imports HOLCF
    11.8  begin

    12.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Mar 04 10:43:39 2009 +0100
    12.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Mar 04 10:45:52 2009 +0100
    12.3 @@ -771,6 +771,55 @@
    12.4  *}
    12.5  
    12.6  
    12.7 +section {* Intuitionistic proof search *}
    12.8 +
    12.9 +text {*
   12.10 +  \begin{matharray}{rcl}
   12.11 +    @{method_def (HOL) iprover} & : & @{text method} \\
   12.12 +  \end{matharray}
   12.13 +
   12.14 +  \begin{rail}
   12.15 +    'iprover' ('!' ?) (rulemod *)
   12.16 +    ;
   12.17 +  \end{rail}
   12.18 +
   12.19 +  The @{method (HOL) iprover} method performs intuitionistic proof
   12.20 +  search, depending on specifically declared rules from the context,
   12.21 +  or given as explicit arguments.  Chained facts are inserted into the
   12.22 +  goal before commencing proof search; ``@{method (HOL) iprover}@{text
   12.23 +  "!"}''  means to include the current @{fact prems} as well.
   12.24 +  
   12.25 +  Rules need to be classified as @{attribute (Pure) intro},
   12.26 +  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
   12.27 +  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
   12.28 +  applied aggressively (without considering back-tracking later).
   12.29 +  Rules declared with ``@{text "?"}'' are ignored in proof search (the
   12.30 +  single-step @{method rule} method still observes these).  An
   12.31 +  explicit weight annotation may be given as well; otherwise the
   12.32 +  number of rule premises will be taken into account here.
   12.33 +*}
   12.34 +
   12.35 +
   12.36 +section {* Coherent Logic *}
   12.37 +
   12.38 +text {*
   12.39 +  \begin{matharray}{rcl}
   12.40 +    @{method_def (HOL) "coherent"} & : & @{text method} \\
   12.41 +  \end{matharray}
   12.42 +
   12.43 +  \begin{rail}
   12.44 +    'coherent' thmrefs?
   12.45 +    ;
   12.46 +  \end{rail}
   12.47 +
   12.48 +  The @{method (HOL) coherent} method solves problems of
   12.49 +  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
   12.50 +  applications in confluence theory, lattice theory and projective
   12.51 +  geometry.  See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
   12.52 +  examples.
   12.53 +*}
   12.54 +
   12.55 +
   12.56  section {* Invoking automated reasoning tools -- The Sledgehammer *}
   12.57  
   12.58  text {*

    13.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Mar 04 10:43:39 2009 +0100
    13.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Mar 04 10:45:52 2009 +0100
    13.3 @@ -1,5 +1,3 @@
    13.4 -(* $Id$ *)
    13.5 -
    13.6  theory Inner_Syntax
    13.7  imports Main
    13.8  begin
    13.9 @@ -370,7 +368,7 @@
   13.10    \end{matharray}
   13.11  
   13.12    \begin{rail}
   13.13 -    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
   13.14 +    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
   13.15      ;
   13.16    \end{rail}
   13.17  
   13.18 @@ -525,13 +523,15 @@
   13.19      & @{text "|"} & @{text "tid  |  tvar  |  "}@{verbatim "_"} \\
   13.20      & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text "sort  |  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
   13.21      & @{text "|"} & @{text "id  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id  |  "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\
   13.22 -    & @{text "|"} & @{text "longid  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid  |  "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\
   13.23 +    & @{text "|"} & @{text "longid  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid"} \\
   13.24 +    & @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\
   13.25      & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
   13.26      & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
   13.27      & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
   13.28      & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\
   13.29  
   13.30 -  @{syntax_def (inner) sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"}@{text "  |  "}@{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\
   13.31 +  @{syntax_def (inner) sort} & = & @{text "id  |  longid  |  "}@{verbatim "{}"} \\
   13.32 +    & @{text "|"} & @{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\
   13.33    \end{supertabular}
   13.34    \end{center}
   13.35  

    14.1 --- a/doc-src/IsarRef/Thy/Introduction.thy	Wed Mar 04 10:43:39 2009 +0100
    14.2 +++ b/doc-src/IsarRef/Thy/Introduction.thy	Wed Mar 04 10:45:52 2009 +0100
    14.3 @@ -1,5 +1,3 @@
    14.4 -(* $Id$ *)
    14.5 -
    14.6  theory Introduction
    14.7  imports Main
    14.8  begin
    14.9 @@ -12,27 +10,27 @@
   14.10    The \emph{Isabelle} system essentially provides a generic
   14.11    infrastructure for building deductive systems (programmed in
   14.12    Standard ML), with a special focus on interactive theorem proving in
   14.13 -  higher-order logics.  In the olden days even end-users would refer
   14.14 -  to certain ML functions (goal commands, tactics, tacticals etc.) to
   14.15 -  pursue their everyday theorem proving tasks
   14.16 -  \cite{isabelle-intro,isabelle-ref}.
   14.17 +  higher-order logics.  Many years ago, even end-users would refer to
   14.18 +  certain ML functions (goal commands, tactics, tacticals etc.) to
   14.19 +  pursue their everyday theorem proving tasks.
   14.20    
   14.21    In contrast \emph{Isar} provides an interpreted language environment
   14.22    of its own, which has been specifically tailored for the needs of
   14.23    theory and proof development.  Compared to raw ML, the Isabelle/Isar
   14.24    top-level provides a more robust and comfortable development
   14.25 -  platform, with proper support for theory development graphs,
   14.26 -  single-step transactions with unlimited undo, etc.  The
   14.27 -  Isabelle/Isar version of the \emph{Proof~General} user interface
   14.28 -  \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
   14.29 -  front-end for interactive theory and proof development in this
   14.30 -  advanced theorem proving environment.
   14.31 +  platform, with proper support for theory development graphs, managed
   14.32 +  transactions with unlimited undo etc.  The Isabelle/Isar version of
   14.33 +  the \emph{Proof~General} user interface
   14.34 +  \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
   14.35 +  for interactive theory and proof development in this advanced
   14.36 +  theorem proving environment, even though it is somewhat biased
   14.37 +  towards old-style proof scripts.
   14.38  
   14.39    \medskip Apart from the technical advances over bare-bones ML
   14.40    programming, the main purpose of the Isar language is to provide a
   14.41    conceptually different view on machine-checked proofs
   14.42 -  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar'' stands for
   14.43 -  ``Intelligible semi-automated reasoning''.  Drawing from both the
   14.44 +  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  \emph{Isar} stands for
   14.45 +  \emph{Intelligible semi-automated reasoning}.  Drawing from both the
   14.46    traditions of informal mathematical proof texts and high-level
   14.47    programming languages, Isar offers a versatile environment for
   14.48    structured formal proof documents.  Thus properly written Isar
   14.49 @@ -47,12 +45,12 @@
   14.50    Despite its grand design of structured proof texts, Isar is able to
   14.51    assimilate the old tactical style as an ``improper'' sub-language.
   14.52    This provides an easy upgrade path for existing tactic scripts, as
   14.53 -  well as additional means for interactive experimentation and
   14.54 -  debugging of structured proofs.  Isabelle/Isar supports a broad
   14.55 -  range of proof styles, both readable and unreadable ones.
   14.56 +  well as some means for interactive experimentation and debugging of
   14.57 +  structured proofs.  Isabelle/Isar supports a broad range of proof
   14.58 +  styles, both readable and unreadable ones.
   14.59  
   14.60 -  \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
   14.61 -  is generic and should work reasonably well for any Isabelle
   14.62 +  \medskip The generic Isabelle/Isar framework (see
   14.63 +  \chref{ch:isar-framework}) works reasonably well for any Isabelle
   14.64    object-logic that conforms to the natural deduction view of the
   14.65    Isabelle/Pure framework.  Specific language elements introduced by
   14.66    the major object-logics are described in \chref{ch:hol}
   14.67 @@ -72,194 +70,4 @@
   14.68    context; other commands emulate old-style tactical theorem proving.
   14.69  *}
   14.70  
   14.71 -
   14.72 -section {* User interfaces *}
   14.73 -
   14.74 -subsection {* Terminal sessions *}
   14.75 -
   14.76 -text {*
   14.77 -  The Isabelle \texttt{tty} tool provides a very interface for running
   14.78 -  the Isar interaction loop, with some support for command line
   14.79 -  editing.  For example:
   14.80 -\begin{ttbox}
   14.81 -isabelle tty\medskip
   14.82 -{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
   14.83 -theory Foo imports Main begin;
   14.84 -definition foo :: nat where "foo == 1";
   14.85 -lemma "0 < foo" by (simp add: foo_def);
   14.86 -end;
   14.87 -\end{ttbox}
   14.88 -
   14.89 -  Any Isabelle/Isar command may be retracted by @{command undo}.
   14.90 -  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
   14.91 -  comprehensive overview of available commands and other language
   14.92 -  elements.
   14.93 -*}
   14.94 -
   14.95 -
   14.96 -subsection {* Emacs Proof General *}
   14.97 -
   14.98 -text {*
   14.99 -  Plain TTY-based interaction as above used to be quite feasible with
  14.100 -  traditional tactic based theorem proving, but developing Isar
  14.101 -  documents really demands some better user-interface support.  The
  14.102 -  Proof~General environment by David Aspinall
  14.103 -  \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
  14.104 -  interface for interactive theorem provers that organizes all the
  14.105 -  cut-and-paste and forward-backward walk through the text in a very
  14.106 -  neat way.  In Isabelle/Isar, the current position within a partial
  14.107 -  proof document is equally important than the actual proof state.
  14.108 -  Thus Proof~General provides the canonical working environment for
  14.109 -  Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
  14.110 -  existing Isar documents) and for production work.
  14.111 -*}
  14.112 -
  14.113 -
  14.114 -subsubsection{* Proof~General as default Isabelle interface *}
  14.115 -
  14.116 -text {*
  14.117 -  The Isabelle interface wrapper script provides an easy way to invoke
  14.118 -  Proof~General (including XEmacs or GNU Emacs).  The default
  14.119 -  configuration of Isabelle is smart enough to detect the
  14.120 -  Proof~General distribution in several canonical places (e.g.\
  14.121 -  @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}).  Thus the
  14.122 -  capital @{verbatim Isabelle} executable would already refer to the
  14.123 -  @{verbatim "ProofGeneral/isar"} interface without further ado.  The
  14.124 -  Isabelle interface script provides several options; pass @{verbatim
  14.125 -  "-?"}  to see its usage.
  14.126 -
  14.127 -  With the proper Isabelle interface setup, Isar documents may now be edited by
  14.128 -  visiting appropriate theory files, e.g.\ 
  14.129 -\begin{ttbox}
  14.130 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
  14.131 -\end{ttbox}
  14.132 -  Beginners may note the tool bar for navigating forward and backward
  14.133 -  through the text (this depends on the local Emacs installation).
  14.134 -  Consult the Proof~General documentation \cite{proofgeneral} for
  14.135 -  further basic command sequences, in particular ``@{verbatim "C-c C-return"}''
  14.136 -  and ``@{verbatim "C-c u"}''.
  14.137 -
  14.138 -  \medskip Proof~General may be also configured manually by giving
  14.139 -  Isabelle settings like this (see also \cite{isabelle-sys}):
  14.140 -
  14.141 -\begin{ttbox}
  14.142 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
  14.143 -PROOFGENERAL_OPTIONS=""
  14.144 -\end{ttbox}
  14.145 -  You may have to change @{verbatim
  14.146 -  "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation
  14.147 -  directory of Proof~General.
  14.148 -
  14.149 -  \medskip Apart from the Isabelle command line, defaults for
  14.150 -  interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
  14.151 -  setting.  For example, the Emacs executable to be used may be
  14.152 -  configured in Isabelle's settings like this:
  14.153 -\begin{ttbox}
  14.154 -PROOFGENERAL_OPTIONS="-p xemacs-mule"  
  14.155 -\end{ttbox}
  14.156 -
  14.157 -  Occasionally, a user's @{verbatim "~/.emacs"} file contains code
  14.158 -  that is incompatible with the (X)Emacs version used by
  14.159 -  Proof~General, causing the interface startup to fail prematurely.
  14.160 -  Here the @{verbatim "-u false"} option helps to get the interface
  14.161 -  process up and running.  Note that additional Lisp customization
  14.162 -  code may reside in @{verbatim "proofgeneral-settings.el"} of
  14.163 -  @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
  14.164 -  "$ISABELLE_HOME_USER/etc"}.
  14.165 -*}
  14.166 -
  14.167 -
  14.168 -subsubsection {* The X-Symbol package *}
  14.169 -
  14.170 -text {*
  14.171 -  Proof~General incorporates a version of the Emacs X-Symbol package
  14.172 -  \cite{x-symbol}, which handles proper mathematical symbols displayed
  14.173 -  on screen.  Pass option @{verbatim "-x true"} to the Isabelle
  14.174 -  interface script, or check the appropriate Proof~General menu
  14.175 -  setting by hand.  The main challenge of getting X-Symbol to work
  14.176 -  properly is the underlying (semi-automated) X11 font setup.
  14.177 -
  14.178 -  \medskip Using proper mathematical symbols in Isabelle theories can
  14.179 -  be very convenient for readability of large formulas.  On the other
  14.180 -  hand, the plain ASCII sources easily become somewhat unintelligible.
  14.181 -  For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
  14.182 -  the default set of Isabelle symbols.  Nevertheless, the Isabelle
  14.183 -  document preparation system (see \chref{ch:document-prep}) will be
  14.184 -  happy to print non-ASCII symbols properly.  It is even possible to
  14.185 -  invent additional notation beyond the display capabilities of Emacs
  14.186 -  and X-Symbol.
  14.187 -*}
  14.188 -
  14.189 -
  14.190 -section {* Isabelle/Isar theories *}
  14.191 -
  14.192 -text {*
  14.193 -  Isabelle/Isar offers the following main improvements over classic
  14.194 -  Isabelle.
  14.195 -
  14.196 -  \begin{enumerate}
  14.197 -  
  14.198 -  \item A \emph{theory format} that integrates specifications and
  14.199 -  proofs, supporting interactive development and unlimited undo
  14.200 -  operation.
  14.201 -  
  14.202 -  \item A \emph{formal proof document language} designed to support
  14.203 -  intelligible semi-automated reasoning.  Instead of putting together
  14.204 -  unreadable tactic scripts, the author is enabled to express the
  14.205 -  reasoning in way that is close to usual mathematical practice.  The
  14.206 -  old tactical style has been assimilated as ``improper'' language
  14.207 -  elements.
  14.208 -  
  14.209 -  \item A simple document preparation system, for typesetting formal
  14.210 -  developments together with informal text.  The resulting
  14.211 -  hyper-linked PDF documents are equally well suited for WWW
  14.212 -  presentation and as printed copies.
  14.213 -
  14.214 -  \end{enumerate}
  14.215 -
  14.216 -  The Isar proof language is embedded into the new theory format as a
  14.217 -  proper sub-language.  Proof mode is entered by stating some
  14.218 -  @{command theorem} or @{command lemma} at the theory level, and
  14.219 -  left again with the final conclusion (e.g.\ via @{command qed}).
  14.220 -  A few theory specification mechanisms also require some proof, such
  14.221 -  as HOL's @{command typedef} which demands non-emptiness of the
  14.222 -  representing sets.
  14.223 -*}
  14.224 -
  14.225 -
  14.226 -section {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
  14.227 -
  14.228 -text {*
  14.229 -  This is one of the key questions, of course.  First of all, the
  14.230 -  tactic script emulation of Isabelle/Isar essentially provides a
  14.231 -  clarified version of the very same unstructured proof style of
  14.232 -  classic Isabelle.  Old-time users should quickly become acquainted
  14.233 -  with that (slightly degenerative) view of Isar.
  14.234 -
  14.235 -  Writing \emph{proper} Isar proof texts targeted at human readers is
  14.236 -  quite different, though.  Experienced users of the unstructured
  14.237 -  style may even have to unlearn some of their habits to master proof
  14.238 -  composition in Isar.  In contrast, new users with less experience in
  14.239 -  old-style tactical proving, but a good understanding of mathematical
  14.240 -  proof in general, often get started easier.
  14.241 -
  14.242 -  \medskip The present text really is only a reference manual on
  14.243 -  Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to
  14.244 -  give some clues of how the concepts introduced here may be put into
  14.245 -  practice.  Especially note that \appref{ap:refcard} provides a quick
  14.246 -  reference card of the most common Isabelle/Isar language elements.
  14.247 -
  14.248 -  Further issues concerning the Isar concepts are covered in the
  14.249 -  literature
  14.250 -  \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
  14.251 -  The author's PhD thesis \cite{Wenzel-PhD} presently provides the
  14.252 -  most complete exposition of Isar foundations, techniques, and
  14.253 -  applications.  A number of example applications are distributed with
  14.254 -  Isabelle, and available via the Isabelle WWW library (e.g.\
  14.255 -  \url{http://isabelle.in.tum.de/library/}).  The ``Archive of Formal
  14.256 -  Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
  14.257 -  examples, both in proper Isar proof style and unstructured tactic
  14.258 -  scripts.
  14.259 -*}
  14.260 -
  14.261  end

    15.1 --- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Wed Mar 04 10:43:39 2009 +0100
    15.2 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Wed Mar 04 10:45:52 2009 +0100
    15.3 @@ -1,5 +1,3 @@
    15.4 -(* $Id$ *)
    15.5 -
    15.6  theory ML_Tactic
    15.7  imports Main
    15.8  begin

    16.1 --- a/doc-src/IsarRef/Thy/Misc.thy	Wed Mar 04 10:43:39 2009 +0100
    16.2 +++ b/doc-src/IsarRef/Thy/Misc.thy	Wed Mar 04 10:45:52 2009 +0100
    16.3 @@ -1,5 +1,3 @@
    16.4 -(* $Id$ *)
    16.5 -
    16.6  theory Misc
    16.7  imports Main
    16.8  begin

    17.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Wed Mar 04 10:43:39 2009 +0100
    17.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Wed Mar 04 10:45:52 2009 +0100
    17.3 @@ -1,5 +1,3 @@
    17.4 -(* $Id$ *)
    17.5 -
    17.6  theory Outer_Syntax
    17.7  imports Main
    17.8  begin
    17.9 @@ -170,10 +168,10 @@
   17.10    Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
   17.11    symbols like this, although proper presentation is left to front-end
   17.12    tools such as {\LaTeX} or Proof~General with the X-Symbol package.
   17.13 -  A list of standard Isabelle symbols that work well with these tools
   17.14 -  is given in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does
   17.15 -  not belong to the @{text letter} category, since it is already used
   17.16 -  differently in the Pure term language.
   17.17 +  A list of predefined Isabelle symbols that work well with these
   17.18 +  tools is given in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"}
   17.19 +  does not belong to the @{text letter} category, since it is already
   17.20 +  used differently in the Pure term language.
   17.21  *}
   17.22  
   17.23  

    18.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Wed Mar 04 10:43:39 2009 +0100
    18.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Wed Mar 04 10:45:52 2009 +0100
    18.3 @@ -1,17 +1,15 @@
    18.4 -(* $Id$ *)
    18.5 -
    18.6  theory Proof
    18.7  imports Main
    18.8  begin
    18.9  
   18.10 -chapter {* Proofs *}
   18.11 +chapter {* Proofs \label{ch:proofs} *}
   18.12  
   18.13  text {*
   18.14    Proof commands perform transitions of Isar/VM machine
   18.15    configurations, which are block-structured, consisting of a stack of
   18.16    nodes with three main components: logical proof context, current
   18.17 -  facts, and open goals.  Isar/VM transitions are \emph{typed}
   18.18 -  according to the following three different modes of operation:
   18.19 +  facts, and open goals.  Isar/VM transitions are typed according to
   18.20 +  the following three different modes of operation:
   18.21  
   18.22    \begin{description}
   18.23  
   18.24 @@ -32,13 +30,17 @@
   18.25  
   18.26    \end{description}
   18.27  
   18.28 -  The proof mode indicator may be read as a verb telling the writer
   18.29 -  what kind of operation may be performed next.  The corresponding
   18.30 -  typings of proof commands restricts the shape of well-formed proof
   18.31 -  texts to particular command sequences.  So dynamic arrangements of
   18.32 -  commands eventually turn out as static texts of a certain structure.
   18.33 -  \Appref{ap:refcard} gives a simplified grammar of the overall
   18.34 -  (extensible) language emerging that way.
   18.35 +  The proof mode indicator may be understood as an instruction to the
   18.36 +  writer, telling what kind of operation may be performed next.  The
   18.37 +  corresponding typings of proof commands restricts the shape of
   18.38 +  well-formed proof texts to particular command sequences.  So dynamic
   18.39 +  arrangements of commands eventually turn out as static texts of a
   18.40 +  certain structure.
   18.41 +
   18.42 +  \Appref{ap:refcard} gives a simplified grammar of the (extensible)
   18.43 +  language emerging that way from the different types of proof
   18.44 +  commands.  The main ideas of the overall Isar framework are
   18.45 +  explained in \chref{ch:isar-framework}.
   18.46  *}
   18.47  
   18.48  
   18.49 @@ -681,7 +683,6 @@
   18.50      @{method_def "assumption"} & : & @{text method} \\
   18.51      @{method_def "this"} & : & @{text method} \\
   18.52      @{method_def "rule"} & : & @{text method} \\
   18.53 -    @{method_def "iprover"} & : & @{text method} \\[0.5ex]
   18.54      @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
   18.55      @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
   18.56      @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
   18.57 @@ -696,8 +697,6 @@
   18.58      ;
   18.59      'rule' thmrefs?
   18.60      ;
   18.61 -    'iprover' ('!' ?) (rulemod *)
   18.62 -    ;
   18.63      rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
   18.64      ;
   18.65      ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
   18.66 @@ -756,27 +755,11 @@
   18.67    default behavior of @{command "proof"} and ``@{command ".."}'' 
   18.68    (double-dot) steps (see \secref{sec:proof-steps}).
   18.69    
   18.70 -  \item @{method iprover} performs intuitionistic proof search,
   18.71 -  depending on specifically declared rules from the context, or given
   18.72 -  as explicit arguments.  Chained facts are inserted into the goal
   18.73 -  before commencing proof search; ``@{method iprover}@{text "!"}''
   18.74 -  means to include the current @{fact prems} as well.
   18.75 -  
   18.76 -  Rules need to be classified as @{attribute (Pure) intro},
   18.77 -  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
   18.78 -  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
   18.79 -  applied aggressively (without considering back-tracking later).
   18.80 -  Rules declared with ``@{text "?"}'' are ignored in proof search (the
   18.81 -  single-step @{method rule} method still observes these).  An
   18.82 -  explicit weight annotation may be given as well; otherwise the
   18.83 -  number of rule premises will be taken into account here.
   18.84 -  
   18.85    \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
   18.86    @{attribute (Pure) dest} declare introduction, elimination, and
   18.87 -  destruct rules, to be used with the @{method rule} and @{method
   18.88 -  iprover} methods.  Note that the latter will ignore rules declared
   18.89 -  with ``@{text "?"}'', while ``@{text "!"}''  are used most
   18.90 -  aggressively.
   18.91 +  destruct rules, to be used with method @{method rule}, and similar
   18.92 +  tools.  Note that the latter will ignore rules declared with
   18.93 +  ``@{text "?"}'', while ``@{text "!"}''  are used most aggressively.
   18.94    
   18.95    The classical reasoner (see \secref{sec:classical}) introduces its
   18.96    own variants of these attributes; use qualified names to access the
   18.97 @@ -963,7 +946,7 @@
   18.98    \begin{matharray}{l}
   18.99      @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n  \<langle>proof\<rangle> \<equiv>"} \\[1ex]
  18.100      \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
  18.101 -    \quad @{command "proof"}~@{text succeed} \\
  18.102 +    \quad @{command "proof"}~@{method succeed} \\
  18.103      \qquad @{command "fix"}~@{text thesis} \\
  18.104      \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
  18.105      \qquad @{command "then"}~@{command "show"}~@{text thesis} \\

    19.1 --- a/doc-src/IsarRef/Thy/Quick_Reference.thy	Wed Mar 04 10:43:39 2009 +0100
    19.2 +++ b/doc-src/IsarRef/Thy/Quick_Reference.thy	Wed Mar 04 10:45:52 2009 +0100
    19.3 @@ -1,5 +1,3 @@
    19.4 -(* $Id$ *)
    19.5 -
    19.6  theory Quick_Reference
    19.7  imports Main
    19.8  begin
    19.9 @@ -30,7 +28,7 @@
   19.10  
   19.11    \begin{tabular}{rcl}
   19.12      @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof  |"}~~@{command "definition"}~@{text "\<dots>  |  \<dots>"} \\[1ex]
   19.13 -    @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
   19.14 +    @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\
   19.15      & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
   19.16      @{text prfx} & = & @{command "apply"}~@{text method} \\
   19.17      & @{text "|"} & @{command "using"}~@{text "facts"} \\

    20.1 --- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed Mar 04 10:43:39 2009 +0100
    20.2 +++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed Mar 04 10:45:52 2009 +0100
    20.3 @@ -1,6 +1,3 @@
    20.4 -
    20.5 -(* $Id$ *)
    20.6 -
    20.7  set ThyOutput.source;
    20.8  use "../../antiquote_setup.ML";
    20.9  

    21.1 --- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed Mar 04 10:43:39 2009 +0100
    21.2 +++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed Mar 04 10:45:52 2009 +0100
    21.3 @@ -1,6 +1,3 @@
    21.4 -
    21.5 -(* $Id$ *)
    21.6 -
    21.7  set ThyOutput.source;
    21.8  use "../../antiquote_setup.ML";
    21.9  

    22.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Wed Mar 04 10:43:39 2009 +0100
    22.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Wed Mar 04 10:45:52 2009 +0100
    22.3 @@ -1,18 +1,20 @@
    22.4 -
    22.5 -(* $Id$ *)
    22.6 -
    22.7 +set quick_and_dirty;
    22.8  set ThyOutput.source;
    22.9  use "../../antiquote_setup.ML";
   22.10  
   22.11 -use_thy "Introduction";
   22.12 -use_thy "Outer_Syntax";
   22.13 -use_thy "Document_Preparation";
   22.14 -use_thy "Spec";
   22.15 -use_thy "Proof";
   22.16 -use_thy "Inner_Syntax";
   22.17 -use_thy "Misc";
   22.18 -use_thy "Generic";
   22.19 -use_thy "HOL_Specific";
   22.20 -use_thy "Quick_Reference";
   22.21 -use_thy "Symbols";
   22.22 -use_thy "ML_Tactic";
   22.23 +use_thys [
   22.24 +  "Introduction",
   22.25 +  "Framework",
   22.26 +  "First_Order_Logic",
   22.27 +  "Outer_Syntax",
   22.28 +  "Document_Preparation",
   22.29 +  "Spec",
   22.30 +  "Proof",
   22.31 +  "Inner_Syntax",
   22.32 +  "Misc",
   22.33 +  "Generic",
   22.34 +  "HOL_Specific",
   22.35 +  "Quick_Reference",
   22.36 +  "Symbols",
   22.37 +  "ML_Tactic"
   22.38 +];

    23.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 04 10:43:39 2009 +0100
    23.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 04 10:45:52 2009 +0100
    23.3 @@ -4,6 +4,24 @@
    23.4  
    23.5  chapter {* Theory specifications *}
    23.6  
    23.7 +text {*
    23.8 +  The Isabelle/Isar theory format integrates specifications and
    23.9 +  proofs, supporting interactive development with unlimited undo
   23.10 +  operation.  There is an integrated document preparation system (see
   23.11 +  \chref{ch:document-prep}), for typesetting formal developments
   23.12 +  together with informal text.  The resulting hyper-linked PDF
   23.13 +  documents can be used both for WWW presentation and printed copies.
   23.14 +
   23.15 +  The Isar proof language (see \chref{ch:proofs}) is embedded into the
   23.16 +  theory language as a proper sub-language.  Proof mode is entered by
   23.17 +  stating some @{command theorem} or @{command lemma} at the theory
   23.18 +  level, and left again with the final conclusion (e.g.\ via @{command
   23.19 +  qed}).  Some theory specification mechanisms also require a proof,
   23.20 +  such as @{command typedef} in HOL, which demands non-emptiness of
   23.21 +  the representing sets.
   23.22 +*}
   23.23 +
   23.24 +
   23.25  section {* Defining theories \label{sec:begin-thy} *}
   23.26  
   23.27  text {*
   23.28 @@ -106,9 +124,9 @@
   23.29    @{command (global) "end"} has a different meaning: it concludes the
   23.30    theory itself (\secref{sec:begin-thy}).
   23.31    
   23.32 -  \item @{text "(\<IN> c)"} given after any local theory command
   23.33 -  specifies an immediate target, e.g.\ ``@{command
   23.34 -  "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
   23.35 +  \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
   23.36 +  local theory command specifies an immediate target, e.g.\
   23.37 +  ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
   23.38    "theorem"}~@{text "(\<IN> c) \<dots>"}''.  This works both in a local or
   23.39    global theory context; the current target context will be suspended
   23.40    for this command only.  Note that ``@{text "(\<IN> -)"}'' will
   23.41 @@ -1164,7 +1182,7 @@
   23.42  
   23.43    \end{description}
   23.44  
   23.45 -  See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
   23.46 +  See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
   23.47    defining a new primitive rule as oracle, and turning it into a proof
   23.48    method.
   23.49  *}

    24.1 --- a/doc-src/IsarRef/Thy/Symbols.thy	Wed Mar 04 10:43:39 2009 +0100
    24.2 +++ b/doc-src/IsarRef/Thy/Symbols.thy	Wed Mar 04 10:45:52 2009 +0100
    24.3 @@ -1,10 +1,8 @@
    24.4 -(* $Id$ *)
    24.5 -
    24.6  theory Symbols
    24.7  imports Pure
    24.8  begin
    24.9  
   24.10 -chapter {* Standard Isabelle symbols \label{app:symbols} *}
   24.11 +chapter {* Predefined Isabelle symbols \label{app:symbols} *}
   24.12  
   24.13  text {*
   24.14    Isabelle supports an infinite number of non-ASCII symbols, which are

    25.1 --- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed Mar 04 10:43:39 2009 +0100
    25.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed Mar 04 10:45:52 2009 +0100
    25.3 @@ -1,5 +1,3 @@
    25.4 -(* $Id$ *)
    25.5 -
    25.6  theory ZF_Specific
    25.7  imports Main
    25.8  begin

    26.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Wed Mar 04 10:43:39 2009 +0100
    26.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Wed Mar 04 10:45:52 2009 +0100
    26.3 @@ -3,8 +3,6 @@
    26.4  \def\isabellecontext{Document{\isacharunderscore}Preparation}%
    26.5  %
    26.6  \isadelimtheory
    26.7 -\isanewline
    26.8 -\isanewline
    26.9  %
   26.10  \endisadelimtheory
   26.11  %

    27.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Wed Mar 04 10:43:39 2009 +0100
    27.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Wed Mar 04 10:45:52 2009 +0100
    27.3 @@ -3,8 +3,6 @@
    27.4  \def\isabellecontext{Generic}%
    27.5  %
    27.6  \isadelimtheory
    27.7 -\isanewline
    27.8 -\isanewline
    27.9  %
   27.10  \endisadelimtheory
   27.11  %

    28.1 --- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Wed Mar 04 10:43:39 2009 +0100
    28.2 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Wed Mar 04 10:45:52 2009 +0100
    28.3 @@ -3,8 +3,6 @@
    28.4  \def\isabellecontext{HOLCF{\isacharunderscore}Specific}%
    28.5  %
    28.6  \isadelimtheory
    28.7 -\isanewline
    28.8 -\isanewline
    28.9  %
   28.10  \endisadelimtheory
   28.11  %

    29.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Mar 04 10:43:39 2009 +0100
    29.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Mar 04 10:45:52 2009 +0100
    29.3 @@ -779,6 +779,58 @@
    29.4  \end{isamarkuptext}%
    29.5  \isamarkuptrue%
    29.6  %
    29.7 +\isamarkupsection{Intuitionistic proof search%
    29.8 +}
    29.9 +\isamarkuptrue%
   29.10 +%
   29.11 +\begin{isamarkuptext}%
   29.12 +\begin{matharray}{rcl}
   29.13 +    \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
   29.14 +  \end{matharray}
   29.15 +
   29.16 +  \begin{rail}
   29.17 +    'iprover' ('!' ?) (rulemod *)
   29.18 +    ;
   29.19 +  \end{rail}
   29.20 +
   29.21 +  The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
   29.22 +  search, depending on specifically declared rules from the context,
   29.23 +  or given as explicit arguments.  Chained facts are inserted into the
   29.24 +  goal before commencing proof search; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
   29.25 +  
   29.26 +  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
   29.27 +  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
   29.28 +  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
   29.29 +  applied aggressively (without considering back-tracking later).
   29.30 +  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
   29.31 +  single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
   29.32 +  explicit weight annotation may be given as well; otherwise the
   29.33 +  number of rule premises will be taken into account here.%
   29.34 +\end{isamarkuptext}%
   29.35 +\isamarkuptrue%
   29.36 +%
   29.37 +\isamarkupsection{Coherent Logic%
   29.38 +}
   29.39 +\isamarkuptrue%
   29.40 +%
   29.41 +\begin{isamarkuptext}%
   29.42 +\begin{matharray}{rcl}
   29.43 +    \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
   29.44 +  \end{matharray}
   29.45 +
   29.46 +  \begin{rail}
   29.47 +    'coherent' thmrefs?
   29.48 +    ;
   29.49 +  \end{rail}
   29.50 +
   29.51 +  The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
   29.52 +  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
   29.53 +  applications in confluence theory, lattice theory and projective
   29.54 +  geometry.  See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Coherent{\isachardot}thy}}}} for some
   29.55 +  examples.%
   29.56 +\end{isamarkuptext}%
   29.57 +\isamarkuptrue%
   29.58 +%
   29.59  \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
   29.60  }
   29.61  \isamarkuptrue%

    30.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Mar 04 10:43:39 2009 +0100
    30.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Mar 04 10:45:52 2009 +0100
    30.3 @@ -3,8 +3,6 @@
    30.4  \def\isabellecontext{Inner{\isacharunderscore}Syntax}%
    30.5  %
    30.6  \isadelimtheory
    30.7 -\isanewline
    30.8 -\isanewline
    30.9  %
   30.10  \endisadelimtheory
   30.11  %
   30.12 @@ -120,19 +118,19 @@
   30.13  %
   30.14  \begin{isamarkuptext}%
   30.15  \begin{mldecls} 
   30.16 -    \indexml{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
   30.17 -    \indexml{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
   30.18 -    \indexml{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
   30.19 -    \indexml{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
   30.20 -    \indexml{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
   30.21 -    \indexml{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
   30.22 -    \indexml{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
   30.23 -    \indexml{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
   30.24 -    \indexml{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
   30.25 -    \indexml{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
   30.26 -    \indexml{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
   30.27 -    \indexml{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
   30.28 -    \indexml{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   30.29 +    \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
   30.30 +    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
   30.31 +    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
   30.32 +    \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
   30.33 +    \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
   30.34 +    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
   30.35 +    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
   30.36 +    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
   30.37 +    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
   30.38 +    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
   30.39 +    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
   30.40 +    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
   30.41 +    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
   30.42    \end{mldecls}
   30.43  
   30.44    These global ML variables control the detail of information that is
   30.45 @@ -233,9 +231,9 @@
   30.46  %
   30.47  \begin{isamarkuptext}%
   30.48  \begin{mldecls}
   30.49 -    \indexml{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
   30.50 -    \indexml{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
   30.51 -    \indexml{print\_depth}\verb|print_depth: int -> unit| \\
   30.52 +    \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
   30.53 +    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
   30.54 +    \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   30.55    \end{mldecls}
   30.56  
   30.57    These ML functions set limits for pretty printed text.
   30.58 @@ -392,7 +390,7 @@
   30.59    \end{matharray}
   30.60  
   30.61    \begin{rail}
   30.62 -    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
   30.63 +    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
   30.64      ;
   30.65    \end{rail}
   30.66  
   30.67 @@ -551,13 +549,15 @@
   30.68      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
   30.69      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\
   30.70      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\
   30.71 -    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
   30.72 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid{\isachardoublequote}} \\
   30.73 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
   30.74      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
   30.75      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
   30.76      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
   30.77      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
   30.78  
   30.79 -  \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
   30.80 +  \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}| \\
   30.81 +    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
   30.82    \end{supertabular}
   30.83    \end{center}
   30.84  

    31.1 --- a/doc-src/IsarRef/Thy/document/Introduction.tex	Wed Mar 04 10:43:39 2009 +0100
    31.2 +++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Wed Mar 04 10:45:52 2009 +0100
    31.3 @@ -3,8 +3,6 @@
    31.4  \def\isabellecontext{Introduction}%
    31.5  %
    31.6  \isadelimtheory
    31.7 -\isanewline
    31.8 -\isanewline
    31.9  %
   31.10  \endisadelimtheory
   31.11  %
   31.12 @@ -32,27 +30,27 @@
   31.13  The \emph{Isabelle} system essentially provides a generic
   31.14    infrastructure for building deductive systems (programmed in
   31.15    Standard ML), with a special focus on interactive theorem proving in
   31.16 -  higher-order logics.  In the olden days even end-users would refer
   31.17 -  to certain ML functions (goal commands, tactics, tacticals etc.) to
   31.18 -  pursue their everyday theorem proving tasks
   31.19 -  \cite{isabelle-intro,isabelle-ref}.
   31.20 +  higher-order logics.  Many years ago, even end-users would refer to
   31.21 +  certain ML functions (goal commands, tactics, tacticals etc.) to
   31.22 +  pursue their everyday theorem proving tasks.
   31.23    
   31.24    In contrast \emph{Isar} provides an interpreted language environment
   31.25    of its own, which has been specifically tailored for the needs of
   31.26    theory and proof development.  Compared to raw ML, the Isabelle/Isar
   31.27    top-level provides a more robust and comfortable development
   31.28 -  platform, with proper support for theory development graphs,
   31.29 -  single-step transactions with unlimited undo, etc.  The
   31.30 -  Isabelle/Isar version of the \emph{Proof~General} user interface
   31.31 -  \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
   31.32 -  front-end for interactive theory and proof development in this
   31.33 -  advanced theorem proving environment.
   31.34 +  platform, with proper support for theory development graphs, managed
   31.35 +  transactions with unlimited undo etc.  The Isabelle/Isar version of
   31.36 +  the \emph{Proof~General} user interface
   31.37 +  \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
   31.38 +  for interactive theory and proof development in this advanced
   31.39 +  theorem proving environment, even though it is somewhat biased
   31.40 +  towards old-style proof scripts.
   31.41  
   31.42    \medskip Apart from the technical advances over bare-bones ML
   31.43    programming, the main purpose of the Isar language is to provide a
   31.44    conceptually different view on machine-checked proofs
   31.45 -  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar'' stands for
   31.46 -  ``Intelligible semi-automated reasoning''.  Drawing from both the
   31.47 +  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  \emph{Isar} stands for
   31.48 +  \emph{Intelligible semi-automated reasoning}.  Drawing from both the
   31.49    traditions of informal mathematical proof texts and high-level
   31.50    programming languages, Isar offers a versatile environment for
   31.51    structured formal proof documents.  Thus properly written Isar
   31.52 @@ -67,12 +65,12 @@
   31.53    Despite its grand design of structured proof texts, Isar is able to
   31.54    assimilate the old tactical style as an ``improper'' sub-language.
   31.55    This provides an easy upgrade path for existing tactic scripts, as
   31.56 -  well as additional means for interactive experimentation and
   31.57 -  debugging of structured proofs.  Isabelle/Isar supports a broad
   31.58 -  range of proof styles, both readable and unreadable ones.
   31.59 +  well as some means for interactive experimentation and debugging of
   31.60 +  structured proofs.  Isabelle/Isar supports a broad range of proof
   31.61 +  styles, both readable and unreadable ones.
   31.62  
   31.63 -  \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
   31.64 -  is generic and should work reasonably well for any Isabelle
   31.65 +  \medskip The generic Isabelle/Isar framework (see
   31.66 +  \chref{ch:isar-framework}) works reasonably well for any Isabelle
   31.67    object-logic that conforms to the natural deduction view of the
   31.68    Isabelle/Pure framework.  Specific language elements introduced by
   31.69    the major object-logics are described in \chref{ch:hol}
   31.70 @@ -92,207 +90,6 @@
   31.71  \end{isamarkuptext}%
   31.72  \isamarkuptrue%
   31.73  %
   31.74 -\isamarkupsection{User interfaces%
   31.75 -}
   31.76 -\isamarkuptrue%
   31.77 -%
   31.78 -\isamarkupsubsection{Terminal sessions%
   31.79 -}
   31.80 -\isamarkuptrue%
   31.81 -%
   31.82 -\begin{isamarkuptext}%
   31.83 -The Isabelle \texttt{tty} tool provides a very interface for running
   31.84 -  the Isar interaction loop, with some support for command line
   31.85 -  editing.  For example:
   31.86 -\begin{ttbox}
   31.87 -isabelle tty\medskip
   31.88 -{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
   31.89 -theory Foo imports Main begin;
   31.90 -definition foo :: nat where "foo == 1";
   31.91 -lemma "0 < foo" by (simp add: foo_def);
   31.92 -end;
   31.93 -\end{ttbox}
   31.94 -
   31.95 -  Any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.
   31.96 -  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
   31.97 -  comprehensive overview of available commands and other language
   31.98 -  elements.%
   31.99 -\end{isamarkuptext}%
  31.100 -\isamarkuptrue%
  31.101 -%
  31.102 -\isamarkupsubsection{Emacs Proof General%
  31.103 -}
  31.104 -\isamarkuptrue%
  31.105 -%
  31.106 -\begin{isamarkuptext}%
  31.107 -Plain TTY-based interaction as above used to be quite feasible with
  31.108 -  traditional tactic based theorem proving, but developing Isar
  31.109 -  documents really demands some better user-interface support.  The
  31.110 -  Proof~General environment by David Aspinall
  31.111 -  \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
  31.112 -  interface for interactive theorem provers that organizes all the
  31.113 -  cut-and-paste and forward-backward walk through the text in a very
  31.114 -  neat way.  In Isabelle/Isar, the current position within a partial
  31.115 -  proof document is equally important than the actual proof state.
  31.116 -  Thus Proof~General provides the canonical working environment for
  31.117 -  Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
  31.118 -  existing Isar documents) and for production work.%
  31.119 -\end{isamarkuptext}%
  31.120 -\isamarkuptrue%
  31.121 -%
  31.122 -\isamarkupsubsubsection{Proof~General as default Isabelle interface%
  31.123 -}
  31.124 -\isamarkuptrue%
  31.125 -%
  31.126 -\begin{isamarkuptext}%
  31.127 -The Isabelle interface wrapper script provides an easy way to invoke
  31.128 -  Proof~General (including XEmacs or GNU Emacs).  The default
  31.129 -  configuration of Isabelle is smart enough to detect the
  31.130 -  Proof~General distribution in several canonical places (e.g.\
  31.131 -  \verb|$ISABELLE_HOME/contrib/ProofGeneral|).  Thus the
  31.132 -  capital \verb|Isabelle| executable would already refer to the
  31.133 -  \verb|ProofGeneral/isar| interface without further ado.  The
  31.134 -  Isabelle interface script provides several options; pass \verb|-?|  to see its usage.
  31.135 -
  31.136 -  With the proper Isabelle interface setup, Isar documents may now be edited by
  31.137 -  visiting appropriate theory files, e.g.\ 
  31.138 -\begin{ttbox}
  31.139 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
  31.140 -\end{ttbox}
  31.141 -  Beginners may note the tool bar for navigating forward and backward
  31.142 -  through the text (this depends on the local Emacs installation).
  31.143 -  Consult the Proof~General documentation \cite{proofgeneral} for
  31.144 -  further basic command sequences, in particular ``\verb|C-c C-return|''
  31.145 -  and ``\verb|C-c u|''.
  31.146 -
  31.147 -  \medskip Proof~General may be also configured manually by giving
  31.148 -  Isabelle settings like this (see also \cite{isabelle-sys}):
  31.149 -
  31.150 -\begin{ttbox}
  31.151 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
  31.152 -PROOFGENERAL_OPTIONS=""
  31.153 -\end{ttbox}
  31.154 -  You may have to change \verb|$ISABELLE_HOME/contrib/ProofGeneral| to the actual installation
  31.155 -  directory of Proof~General.
  31.156 -
  31.157 -  \medskip Apart from the Isabelle command line, defaults for
  31.158 -  interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
  31.159 -  setting.  For example, the Emacs executable to be used may be
  31.160 -  configured in Isabelle's settings like this:
  31.161 -\begin{ttbox}
  31.162 -PROOFGENERAL_OPTIONS="-p xemacs-mule"  
  31.163 -\end{ttbox}
  31.164 -
  31.165 -  Occasionally, a user's \verb|~/.emacs| file contains code
  31.166 -  that is incompatible with the (X)Emacs version used by
  31.167 -  Proof~General, causing the interface startup to fail prematurely.
  31.168 -  Here the \verb|-u false| option helps to get the interface
  31.169 -  process up and running.  Note that additional Lisp customization
  31.170 -  code may reside in \verb|proofgeneral-settings.el| of
  31.171 -  \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
  31.172 -\end{isamarkuptext}%
  31.173 -\isamarkuptrue%
  31.174 -%
  31.175 -\isamarkupsubsubsection{The X-Symbol package%
  31.176 -}
  31.177 -\isamarkuptrue%
  31.178 -%
  31.179 -\begin{isamarkuptext}%
  31.180 -Proof~General incorporates a version of the Emacs X-Symbol package
  31.181 -  \cite{x-symbol}, which handles proper mathematical symbols displayed
  31.182 -  on screen.  Pass option \verb|-x true| to the Isabelle
  31.183 -  interface script, or check the appropriate Proof~General menu
  31.184 -  setting by hand.  The main challenge of getting X-Symbol to work
  31.185 -  properly is the underlying (semi-automated) X11 font setup.
  31.186 -
  31.187 -  \medskip Using proper mathematical symbols in Isabelle theories can
  31.188 -  be very convenient for readability of large formulas.  On the other
  31.189 -  hand, the plain ASCII sources easily become somewhat unintelligible.
  31.190 -  For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
  31.191 -  the default set of Isabelle symbols.  Nevertheless, the Isabelle
  31.192 -  document preparation system (see \chref{ch:document-prep}) will be
  31.193 -  happy to print non-ASCII symbols properly.  It is even possible to
  31.194 -  invent additional notation beyond the display capabilities of Emacs
  31.195 -  and X-Symbol.%
  31.196 -\end{isamarkuptext}%
  31.197 -\isamarkuptrue%
  31.198 -%
  31.199 -\isamarkupsection{Isabelle/Isar theories%
  31.200 -}
  31.201 -\isamarkuptrue%
  31.202 -%
  31.203 -\begin{isamarkuptext}%
  31.204 -Isabelle/Isar offers the following main improvements over classic
  31.205 -  Isabelle.
  31.206 -
  31.207 -  \begin{enumerate}
  31.208 -  
  31.209 -  \item A \emph{theory format} that integrates specifications and
  31.210 -  proofs, supporting interactive development and unlimited undo
  31.211 -  operation.
  31.212 -  
  31.213 -  \item A \emph{formal proof document language} designed to support
  31.214 -  intelligible semi-automated reasoning.  Instead of putting together
  31.215 -  unreadable tactic scripts, the author is enabled to express the
  31.216 -  reasoning in way that is close to usual mathematical practice.  The
  31.217 -  old tactical style has been assimilated as ``improper'' language
  31.218 -  elements.
  31.219 -  
  31.220 -  \item A simple document preparation system, for typesetting formal
  31.221 -  developments together with informal text.  The resulting
  31.222 -  hyper-linked PDF documents are equally well suited for WWW
  31.223 -  presentation and as printed copies.
  31.224 -
  31.225 -  \end{enumerate}
  31.226 -
  31.227 -  The Isar proof language is embedded into the new theory format as a
  31.228 -  proper sub-language.  Proof mode is entered by stating some
  31.229 -  \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
  31.230 -  left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
  31.231 -  A few theory specification mechanisms also require some proof, such
  31.232 -  as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
  31.233 -  representing sets.%
  31.234 -\end{isamarkuptext}%
  31.235 -\isamarkuptrue%
  31.236 -%
  31.237 -\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
  31.238 -}
  31.239 -\isamarkuptrue%
  31.240 -%
  31.241 -\begin{isamarkuptext}%
  31.242 -This is one of the key questions, of course.  First of all, the
  31.243 -  tactic script emulation of Isabelle/Isar essentially provides a
  31.244 -  clarified version of the very same unstructured proof style of
  31.245 -  classic Isabelle.  Old-time users should quickly become acquainted
  31.246 -  with that (slightly degenerative) view of Isar.
  31.247 -
  31.248 -  Writing \emph{proper} Isar proof texts targeted at human readers is
  31.249 -  quite different, though.  Experienced users of the unstructured
  31.250 -  style may even have to unlearn some of their habits to master proof
  31.251 -  composition in Isar.  In contrast, new users with less experience in
  31.252 -  old-style tactical proving, but a good understanding of mathematical
  31.253 -  proof in general, often get started easier.
  31.254 -
  31.255 -  \medskip The present text really is only a reference manual on
  31.256 -  Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to
  31.257 -  give some clues of how the concepts introduced here may be put into
  31.258 -  practice.  Especially note that \appref{ap:refcard} provides a quick
  31.259 -  reference card of the most common Isabelle/Isar language elements.
  31.260 -
  31.261 -  Further issues concerning the Isar concepts are covered in the
  31.262 -  literature
  31.263 -  \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
  31.264 -  The author's PhD thesis \cite{Wenzel-PhD} presently provides the
  31.265 -  most complete exposition of Isar foundations, techniques, and
  31.266 -  applications.  A number of example applications are distributed with
  31.267 -  Isabelle, and available via the Isabelle WWW library (e.g.\
  31.268 -  \url{http://isabelle.in.tum.de/library/}).  The ``Archive of Formal
  31.269 -  Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
  31.270 -  examples, both in proper Isar proof style and unstructured tactic
  31.271 -  scripts.%
  31.272 -\end{isamarkuptext}%
  31.273 -\isamarkuptrue%
  31.274 -%
  31.275  \isadelimtheory
  31.276  %
  31.277  \endisadelimtheory

    32.1 --- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Wed Mar 04 10:43:39 2009 +0100
    32.2 +++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Wed Mar 04 10:45:52 2009 +0100
    32.3 @@ -3,8 +3,6 @@
    32.4  \def\isabellecontext{ML{\isacharunderscore}Tactic}%
    32.5  %
    32.6  \isadelimtheory
    32.7 -\isanewline
    32.8 -\isanewline
    32.9  %
   32.10  \endisadelimtheory
   32.11  %

    33.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex	Wed Mar 04 10:43:39 2009 +0100
    33.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex	Wed Mar 04 10:45:52 2009 +0100
    33.3 @@ -3,8 +3,6 @@
    33.4  \def\isabellecontext{Misc}%
    33.5  %
    33.6  \isadelimtheory
    33.7 -\isanewline
    33.8 -\isanewline
    33.9  %
   33.10  \endisadelimtheory
   33.11  %

    34.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Wed Mar 04 10:43:39 2009 +0100
    34.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Wed Mar 04 10:45:52 2009 +0100
    34.3 @@ -3,8 +3,6 @@
    34.4  \def\isabellecontext{Outer{\isacharunderscore}Syntax}%
    34.5  %
    34.6  \isadelimtheory
    34.7 -\isanewline
    34.8 -\isanewline
    34.9  %
   34.10  \endisadelimtheory
   34.11  %
   34.12 @@ -185,10 +183,10 @@
   34.13    Isabelle as \verb|\<forall>|.  There are infinitely many Isabelle
   34.14    symbols like this, although proper presentation is left to front-end
   34.15    tools such as {\LaTeX} or Proof~General with the X-Symbol package.
   34.16 -  A list of standard Isabelle symbols that work well with these tools
   34.17 -  is given in \appref{app:symbols}.  Note that \verb|\<lambda>| does
   34.18 -  not belong to the \isa{letter} category, since it is already used
   34.19 -  differently in the Pure term language.%
   34.20 +  A list of predefined Isabelle symbols that work well with these
   34.21 +  tools is given in \appref{app:symbols}.  Note that \verb|\<lambda>|
   34.22 +  does not belong to the \isa{letter} category, since it is already
   34.23 +  used differently in the Pure term language.%
   34.24  \end{isamarkuptext}%
   34.25  \isamarkuptrue%
   34.26  %

    35.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Wed Mar 04 10:43:39 2009 +0100
    35.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Wed Mar 04 10:45:52 2009 +0100
    35.3 @@ -3,8 +3,6 @@
    35.4  \def\isabellecontext{Proof}%
    35.5  %
    35.6  \isadelimtheory
    35.7 -\isanewline
    35.8 -\isanewline
    35.9  %
   35.10  \endisadelimtheory
   35.11  %
   35.12 @@ -20,7 +18,7 @@
   35.13  %
   35.14  \endisadelimtheory
   35.15  %
   35.16 -\isamarkupchapter{Proofs%
   35.17 +\isamarkupchapter{Proofs \label{ch:proofs}%
   35.18  }
   35.19  \isamarkuptrue%
   35.20  %
   35.21 @@ -28,8 +26,8 @@
   35.22  Proof commands perform transitions of Isar/VM machine
   35.23    configurations, which are block-structured, consisting of a stack of
   35.24    nodes with three main components: logical proof context, current
   35.25 -  facts, and open goals.  Isar/VM transitions are \emph{typed}
   35.26 -  according to the following three different modes of operation:
   35.27 +  facts, and open goals.  Isar/VM transitions are typed according to
   35.28 +  the following three different modes of operation:
   35.29  
   35.30    \begin{description}
   35.31  
   35.32 @@ -49,13 +47,17 @@
   35.33  
   35.34    \end{description}
   35.35  
   35.36 -  The proof mode indicator may be read as a verb telling the writer
   35.37 -  what kind of operation may be performed next.  The corresponding
   35.38 -  typings of proof commands restricts the shape of well-formed proof
   35.39 -  texts to particular command sequences.  So dynamic arrangements of
   35.40 -  commands eventually turn out as static texts of a certain structure.
   35.41 -  \Appref{ap:refcard} gives a simplified grammar of the overall
   35.42 -  (extensible) language emerging that way.%
   35.43 +  The proof mode indicator may be understood as an instruction to the
   35.44 +  writer, telling what kind of operation may be performed next.  The
   35.45 +  corresponding typings of proof commands restricts the shape of
   35.46 +  well-formed proof texts to particular command sequences.  So dynamic
   35.47 +  arrangements of commands eventually turn out as static texts of a
   35.48 +  certain structure.
   35.49 +
   35.50 +  \Appref{ap:refcard} gives a simplified grammar of the (extensible)
   35.51 +  language emerging that way from the different types of proof
   35.52 +  commands.  The main ideas of the overall Isar framework are
   35.53 +  explained in \chref{ch:isar-framework}.%
   35.54  \end{isamarkuptext}%
   35.55  \isamarkuptrue%
   35.56  %
   35.57 @@ -691,7 +693,6 @@
   35.58      \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
   35.59      \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
   35.60      \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
   35.61 -    \indexdef{}{method}{iprover}\hypertarget{method.iprover}{\hyperlink{method.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\[0.5ex]
   35.62      \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
   35.63      \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
   35.64      \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
   35.65 @@ -706,8 +707,6 @@
   35.66      ;
   35.67      'rule' thmrefs?
   35.68      ;
   35.69 -    'iprover' ('!' ?) (rulemod *)
   35.70 -    ;
   35.71      rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
   35.72      ;
   35.73      ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
   35.74 @@ -762,26 +761,11 @@
   35.75    default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' 
   35.76    (double-dot) steps (see \secref{sec:proof-steps}).
   35.77    
   35.78 -  \item \hyperlink{method.iprover}{\mbox{\isa{iprover}}} performs intuitionistic proof search,
   35.79 -  depending on specifically declared rules from the context, or given
   35.80 -  as explicit arguments.  Chained facts are inserted into the goal
   35.81 -  before commencing proof search; ``\hyperlink{method.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
   35.82 -  means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
   35.83 -  
   35.84 -  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
   35.85 -  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
   35.86 -  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
   35.87 -  applied aggressively (without considering back-tracking later).
   35.88 -  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
   35.89 -  single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
   35.90 -  explicit weight annotation may be given as well; otherwise the
   35.91 -  number of rule premises will be taken into account here.
   35.92 -  
   35.93    \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
   35.94    \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
   35.95 -  destruct rules, to be used with the \hyperlink{method.rule}{\mbox{\isa{rule}}} and \hyperlink{method.iprover}{\mbox{\isa{iprover}}} methods.  Note that the latter will ignore rules declared
   35.96 -  with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most
   35.97 -  aggressively.
   35.98 +  destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
   35.99 +  tools.  Note that the latter will ignore rules declared with
  35.100 +  ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most aggressively.
  35.101    
  35.102    The classical reasoner (see \secref{sec:classical}) introduces its
  35.103    own variants of these attributes; use qualified names to access the
  35.104 @@ -966,7 +950,7 @@
  35.105    \begin{matharray}{l}
  35.106      \isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex]
  35.107      \quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
  35.108 -    \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{succeed} \\
  35.109 +    \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.succeed}{\mbox{\isa{succeed}}} \\
  35.110      \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\
  35.111      \qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
  35.112      \qquad \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis} \\

    36.1 --- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Wed Mar 04 10:43:39 2009 +0100
    36.2 +++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Wed Mar 04 10:45:52 2009 +0100
    36.3 @@ -3,8 +3,6 @@
    36.4  \def\isabellecontext{Quick{\isacharunderscore}Reference}%
    36.5  %
    36.6  \isadelimtheory
    36.7 -\isanewline
    36.8 -\isanewline
    36.9  %
   36.10  \endisadelimtheory
   36.11  %
   36.12 @@ -52,7 +50,7 @@
   36.13  
   36.14    \begin{tabular}{rcl}
   36.15      \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof\ \ {\isacharbar}{\isachardoublequote}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isasymdots}\ \ {\isacharbar}\ \ {\isasymdots}{\isachardoublequote}} \\[1ex]
   36.16 -    \isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}method\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{method} \\
   36.17 +    \isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}method\isactrlsup {\isacharquery}\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}method\isactrlsup {\isacharquery}{\isachardoublequote}} \\
   36.18      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\[1ex]
   36.19      \isa{prfx} & = & \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method} \\
   36.20      & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\

    37.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Mar 04 10:43:39 2009 +0100
    37.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Mar 04 10:45:52 2009 +0100
    37.3 @@ -22,6 +22,23 @@
    37.4  }
    37.5  \isamarkuptrue%
    37.6  %
    37.7 +\begin{isamarkuptext}%
    37.8 +The Isabelle/Isar theory format integrates specifications and
    37.9 +  proofs, supporting interactive development with unlimited undo
   37.10 +  operation.  There is an integrated document preparation system (see
   37.11 +  \chref{ch:document-prep}), for typesetting formal developments
   37.12 +  together with informal text.  The resulting hyper-linked PDF
   37.13 +  documents can be used both for WWW presentation and printed copies.
   37.14 +
   37.15 +  The Isar proof language (see \chref{ch:proofs}) is embedded into the
   37.16 +  theory language as a proper sub-language.  Proof mode is entered by
   37.17 +  stating some \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory
   37.18 +  level, and left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).  Some theory specification mechanisms also require a proof,
   37.19 +  such as \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} in HOL, which demands non-emptiness of
   37.20 +  the representing sets.%
   37.21 +\end{isamarkuptext}%
   37.22 +\isamarkuptrue%
   37.23 +%
   37.24  \isamarkupsection{Defining theories \label{sec:begin-thy}%
   37.25  }
   37.26  \isamarkuptrue%
   37.27 @@ -127,8 +144,9 @@
   37.28    \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
   37.29    theory itself (\secref{sec:begin-thy}).
   37.30    
   37.31 -  \item \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}} given after any local theory command
   37.32 -  specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or
   37.33 +  \item \isa{{\isachardoublequote}{\isacharparenleft}{\isachardoublequote}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isachardoublequote}c{\isacharparenright}{\isachardoublequote}} given after any
   37.34 +  local theory command specifies an immediate target, e.g.\
   37.35 +  ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or
   37.36    global theory context; the current target context will be suspended
   37.37    for this command only.  Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
   37.38    always produce a global result independently of the current target
   37.39 @@ -792,8 +810,8 @@
   37.40    \end{matharray}
   37.41  
   37.42    \begin{mldecls}
   37.43 -    \indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
   37.44 -    \indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   37.45 +    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
   37.46 +    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   37.47    \end{mldecls}
   37.48  
   37.49    \begin{rail}
   37.50 @@ -1178,7 +1196,7 @@
   37.51  
   37.52    \end{description}
   37.53  
   37.54 -  See \hyperlink{file.~~/src/FOL/ex/IffOracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}IffOracle{\isachardot}thy}}}} for a worked example of
   37.55 +  See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
   37.56    defining a new primitive rule as oracle, and turning it into a proof
   37.57    method.%
   37.58  \end{isamarkuptext}%

    38.1 --- a/doc-src/IsarRef/Thy/document/Symbols.tex	Wed Mar 04 10:43:39 2009 +0100
    38.2 +++ b/doc-src/IsarRef/Thy/document/Symbols.tex	Wed Mar 04 10:45:52 2009 +0100
    38.3 @@ -3,8 +3,6 @@
    38.4  \def\isabellecontext{Symbols}%
    38.5  %
    38.6  \isadelimtheory
    38.7 -\isanewline
    38.8 -\isanewline
    38.9  %
   38.10  \endisadelimtheory
   38.11  %
   38.12 @@ -20,7 +18,7 @@
   38.13  %
   38.14  \endisadelimtheory
   38.15  %
   38.16 -\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
   38.17 +\isamarkupchapter{Predefined Isabelle symbols \label{app:symbols}%
   38.18  }
   38.19  \isamarkuptrue%
   38.20  %

    39.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Wed Mar 04 10:43:39 2009 +0100
    39.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Wed Mar 04 10:45:52 2009 +0100
    39.3 @@ -3,8 +3,6 @@
    39.4  \def\isabellecontext{ZF{\isacharunderscore}Specific}%
    39.5  %
    39.6  \isadelimtheory
    39.7 -\isanewline
    39.8 -\isanewline
    39.9  %
   39.10  \endisadelimtheory
   39.11  %

    40.1 --- a/doc-src/IsarRef/isar-ref.tex	Wed Mar 04 10:43:39 2009 +0100
    40.2 +++ b/doc-src/IsarRef/isar-ref.tex	Wed Mar 04 10:45:52 2009 +0100
    40.3 @@ -1,6 +1,3 @@
    40.4 -
    40.5 -%% $Id$
    40.6 -
    40.7  \documentclass[12pt,a4paper,fleqn]{report}
    40.8  \usepackage{amssymb}
    40.9  \usepackage[greek,english]{babel}
   40.10 @@ -27,12 +24,13 @@
   40.11    With Contributions by
   40.12    Clemens Ballarin,
   40.13    Stefan Berghofer, \\
   40.14 +  Timothy Bourke
   40.15    Lucas Dixon,
   40.16 -  Florian Haftmann,
   40.17 -  Gerwin Klein, \\
   40.18 +  Florian Haftmann, \\
   40.19 +  Gerwin Klein,
   40.20    Alexander Krauss,
   40.21 -  Tobias Nipkow,
   40.22 -  David von Oheimb, \\
   40.23 +  Tobias Nipkow, \\
   40.24 +  David von Oheimb,
   40.25    Larry Paulson,
   40.26    and Sebastian Skalberg
   40.27  }
   40.28 @@ -82,7 +80,11 @@
   40.29  
   40.30  \pagenumbering{roman} \tableofcontents \clearfirst
   40.31  
   40.32 +\part{Basic Concepts}
   40.33  \input{Thy/document/Introduction.tex}
   40.34 +\input{Thy/document/Framework.tex}
   40.35 +\input{Thy/document/First_Order_Logic.tex}
   40.36 +\part{General Language Elements}
   40.37  \input{Thy/document/Outer_Syntax.tex}
   40.38  \input{Thy/document/Document_Preparation.tex}
   40.39  \input{Thy/document/Spec.tex}
   40.40 @@ -90,10 +92,12 @@
   40.41  \input{Thy/document/Inner_Syntax.tex}
   40.42  \input{Thy/document/Misc.tex}
   40.43  \input{Thy/document/Generic.tex}
   40.44 +\part{Object-Logics}
   40.45  \input{Thy/document/HOL_Specific.tex}
   40.46  \input{Thy/document/HOLCF_Specific.tex}
   40.47  \input{Thy/document/ZF_Specific.tex}
   40.48  
   40.49 +\part{Appendix}
   40.50  \appendix
   40.51  \input{Thy/document/Quick_Reference.tex}
   40.52  \let\int\intorig
   40.53 @@ -101,7 +105,7 @@
   40.54  \input{Thy/document/ML_Tactic.tex}
   40.55  
   40.56  \begingroup
   40.57 -  \bibliographystyle{plain} \small\raggedright\frenchspacing
   40.58 +  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
   40.59    \bibliography{../manual}
   40.60  \endgroup
   40.61  

    41.1 --- a/doc-src/IsarRef/style.sty	Wed Mar 04 10:43:39 2009 +0100
    41.2 +++ b/doc-src/IsarRef/style.sty	Wed Mar 04 10:45:52 2009 +0100
    41.3 @@ -1,6 +1,3 @@
    41.4 -
    41.5 -%% $Id$
    41.6 -
    41.7  %% toc
    41.8  \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
    41.9  \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
   41.10 @@ -18,12 +15,17 @@
   41.11  
   41.12  %% ML
   41.13  \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
   41.14 -\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
   41.15 +
   41.16 +%% Isar
   41.17 +\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
   41.18 +\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
   41.19  
   41.20  %% math
   41.21 +\newcommand{\isasymstrut}{\isamath{\mathstrut}}
   41.22 +\newcommand{\isasymvartheta}{\isamath{\,\theta}}
   41.23  \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
   41.24  \renewcommand{\isadigit}[1]{\isamath{#1}}
   41.25 -
   41.26 +\newcommand{\text}[1]{\mbox{#1}}
   41.27  
   41.28  %% global style options
   41.29  \pagestyle{headings}

    42.1 --- a/doc-src/Ref/Makefile	Wed Mar 04 10:43:39 2009 +0100
    42.2 +++ b/doc-src/Ref/Makefile	Wed Mar 04 10:45:52 2009 +0100
    42.3 @@ -1,6 +1,3 @@
    42.4 -#
    42.5 -# $Id$
    42.6 -#
    42.7  
    42.8  ## targets
    42.9  
   42.10 @@ -12,16 +9,15 @@
   42.11  include ../Makefile.in
   42.12  
   42.13  NAME = ref
   42.14 -FILES = ref.tex introduction.tex goals.tex tactic.tex tctical.tex \
   42.15 -	thm.tex theories.tex defining.tex syntax.tex substitution.tex \
   42.16 -	simplifier.tex classical.tex theory-syntax.tex \
   42.17 -	../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
   42.18 +FILES = ref.tex introduction.tex tactic.tex tctical.tex thm.tex	\
   42.19 +	theories.tex defining.tex syntax.tex substitution.tex	\
   42.20 +	simplifier.tex classical.tex ../proof.sty ../iman.sty	\
   42.21 +	../extra.sty ../ttbox.sty ../manual.bib
   42.22  
   42.23  dvi: $(NAME).dvi
   42.24  
   42.25  $(NAME).dvi: $(FILES) isabelle.eps
   42.26  	$(LATEX) $(NAME)
   42.27 -	$(RAIL) $(NAME)
   42.28  	$(BIBTEX) $(NAME)
   42.29  	$(LATEX) $(NAME)
   42.30  	$(LATEX) $(NAME)
   42.31 @@ -32,7 +28,6 @@
   42.32  
   42.33  $(NAME).pdf: $(FILES) isabelle.pdf
   42.34  	$(PDFLATEX) $(NAME)
   42.35 -	$(RAIL) $(NAME)
   42.36  	$(BIBTEX) $(NAME)
   42.37  	$(PDFLATEX) $(NAME)
   42.38  	$(PDFLATEX) $(NAME)

    43.1 --- a/doc-src/Ref/classical.tex	Wed Mar 04 10:43:39 2009 +0100
    43.2 +++ b/doc-src/Ref/classical.tex	Wed Mar 04 10:45:52 2009 +0100
    43.3 @@ -1,4 +1,4 @@
    43.4 -%% $Id$
    43.5 +
    43.6  \chapter{The Classical Reasoner}\label{chap:classical}
    43.7  \index{classical reasoner|(}
    43.8  \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
    43.9 @@ -28,29 +28,6 @@
   43.10  be traced, and their components can be called directly; in this manner,
   43.11  any proof can be viewed interactively.
   43.12  
   43.13 -The simplest way to apply the classical reasoner (to subgoal~$i$) is to type
   43.14 -\begin{ttbox}
   43.15 -by (Blast_tac \(i\));
   43.16 -\end{ttbox}
   43.17 -This command quickly proves most simple formulas of the predicate calculus or
   43.18 -set theory.  To attempt to prove subgoals using a combination of
   43.19 -rewriting and classical reasoning, try
   43.20 -\begin{ttbox}
   43.21 -auto();                         \emph{\textrm{applies to all subgoals}}
   43.22 -force i;                        \emph{\textrm{applies to one subgoal}}
   43.23 -\end{ttbox}
   43.24 -To do all obvious logical steps, even if they do not prove the
   43.25 -subgoal, type one of the following:
   43.26 -\begin{ttbox}
   43.27 -by Safe_tac;                   \emph{\textrm{applies to all subgoals}}
   43.28 -by (Clarify_tac \(i\));            \emph{\textrm{applies to one subgoal}}
   43.29 -\end{ttbox}
   43.30 -
   43.31 -
   43.32 -You need to know how the classical reasoner works in order to use it
   43.33 -effectively.  There are many tactics to choose from, including 
   43.34 -{\tt Fast_tac} and \texttt{Best_tac}.
   43.35 -
   43.36  We shall first discuss the underlying principles, then present the classical
   43.37  reasoner.  Finally, we shall see how to instantiate it for new logics.  The
   43.38  logics FOL, ZF, HOL and HOLCF have it already installed.

    44.1 --- a/doc-src/Ref/defining.tex	Wed Mar 04 10:43:39 2009 +0100
    44.2 +++ b/doc-src/Ref/defining.tex	Wed Mar 04 10:45:52 2009 +0100
    44.3 @@ -1,376 +1,5 @@
    44.4 -%% $Id$
    44.5 +
    44.6  \chapter{Defining Logics} \label{Defining-Logics}
    44.7 -This chapter explains how to define new formal systems --- in particular,
    44.8 -their concrete syntax.  While Isabelle can be regarded as a theorem prover
    44.9 -for set theory, higher-order logic or the sequent calculus, its
   44.10 -distinguishing feature is support for the definition of new logics.
   44.11 -
   44.12 -Isabelle logics are hierarchies of theories, which are described and
   44.13 -illustrated in
   44.14 -\iflabelundefined{sec:defining-theories}{{\em Introduction to Isabelle}}%
   44.15 -{\S\ref{sec:defining-theories}}.  That material, together with the theory
   44.16 -files provided in the examples directories, should suffice for all simple
   44.17 -applications.  The easiest way to define a new theory is by modifying a
   44.18 -copy of an existing theory.
   44.19 -
   44.20 -This chapter documents the meta-logic syntax, mixfix declarations and
   44.21 -pretty printing.  The extended examples in \S\ref{sec:min_logics}
   44.22 -demonstrate the logical aspects of the definition of theories.
   44.23 -
   44.24 -
   44.25 -\section{Priority grammars} \label{sec:priority_grammars}
   44.26 -\index{priority grammars|(}
   44.27 -
   44.28 -A context-free grammar contains a set of {\bf nonterminal symbols}, a set of
   44.29 -{\bf terminal symbols} and a set of {\bf productions}\index{productions}.
   44.30 -Productions have the form ${A=\gamma}$, where $A$ is a nonterminal and
   44.31 -$\gamma$ is a string of terminals and nonterminals.  One designated
   44.32 -nonterminal is called the {\bf start symbol}.  The language defined by the
   44.33 -grammar consists of all strings of terminals that can be derived from the
   44.34 -start symbol by applying productions as rewrite rules.
   44.35 -
   44.36 -The syntax of an Isabelle logic is specified by a {\bf priority
   44.37 -  grammar}.\index{priorities} Each nonterminal is decorated by an integer
   44.38 -priority, as in~$A^{(p)}$.  A nonterminal $A^{(p)}$ in a derivation may be
   44.39 -rewritten using a production $A^{(q)} = \gamma$ only if~$p \leq q$.  Any
   44.40 -priority grammar can be translated into a normal context free grammar by
   44.41 -introducing new nonterminals and productions.
   44.42 -
   44.43 -Formally, a set of context free productions $G$ induces a derivation
   44.44 -relation $\longrightarrow@G$.  Let $\alpha$ and $\beta$ denote strings of
   44.45 -terminal or nonterminal symbols.  Then
   44.46 -\[ \alpha\, A^{(p)}\, \beta ~\longrightarrow@G~ \alpha\,\gamma\,\beta \]
   44.47 -if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \leq q$.
   44.48 -
   44.49 -The following simple grammar for arithmetic expressions demonstrates how
   44.50 -binding power and associativity of operators can be enforced by priorities.
   44.51 -\begin{center}
   44.52 -\begin{tabular}{rclr}
   44.53 -  $A^{(9)}$ & = & {\tt0} \\
   44.54 -  $A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
   44.55 -  $A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
   44.56 -  $A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
   44.57 -  $A^{(3)}$ & = & {\tt-} $A^{(3)}$
   44.58 -\end{tabular}
   44.59 -\end{center}
   44.60 -The choice of priorities determines that {\tt -} binds tighter than {\tt *},
   44.61 -which binds tighter than {\tt +}.  Furthermore {\tt +} associates to the
   44.62 -left and {\tt *} to the right.
   44.63 -
   44.64 -For clarity, grammars obey these conventions:
   44.65 -\begin{itemize}
   44.66 -\item All priorities must lie between~0 and \ttindex{max_pri}, which is a
   44.67 -  some fixed integer.  Sometimes {\tt max_pri} is written as $\infty$.
   44.68 -\item Priority 0 on the right-hand side and priority \ttindex{max_pri} on
   44.69 -  the left-hand side may be omitted.
   44.70 -\item The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$; the
   44.71 -  priority of the left-hand side actually appears in a column on the far
   44.72 -  right.
   44.73 -\item Alternatives are separated by~$|$.
   44.74 -\item Repetition is indicated by dots~(\dots) in an informal but obvious
   44.75 -  way.
   44.76 -\end{itemize}
   44.77 -
   44.78 -Using these conventions and assuming $\infty=9$, the grammar
   44.79 -takes the form
   44.80 -\begin{center}
   44.81 -\begin{tabular}{rclc}
   44.82 -$A$ & = & {\tt0} & \hspace*{4em} \\
   44.83 - & $|$ & {\tt(} $A$ {\tt)} \\
   44.84 - & $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
   44.85 - & $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
   44.86 - & $|$ & {\tt-} $A^{(3)}$ & (3)
   44.87 -\end{tabular}
   44.88 -\end{center}
   44.89 -\index{priority grammars|)}
   44.90 -
   44.91 -
   44.92 -\begin{figure}\small
   44.93 -\begin{center}
   44.94 -\begin{tabular}{rclc}
   44.95 -$any$ &=& $prop$ ~~$|$~~ $logic$ \\\\
   44.96 -$prop$ &=& {\tt(} $prop$ {\tt)} \\
   44.97 -     &$|$& $prop^{(4)}$ {\tt::} $type$ & (3) \\
   44.98 -     &$|$& {\tt PROP} $aprop$ \\
   44.99 -     &$|$& $any^{(3)}$ {\tt ==} $any^{(2)}$ & (2) \\
  44.100 -     &$|$& $any^{(3)}$ {\tt =?=} $any^{(2)}$ & (2) \\
  44.101 -     &$|$& $prop^{(2)}$ {\tt ==>} $prop^{(1)}$ & (1) \\
  44.102 -     &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\
  44.103 -     &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\
  44.104 -     &$|$& {\tt OFCLASS} {\tt(} $type$ {\tt,} $logic$ {\tt)} \\\\
  44.105 -$aprop$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$
  44.106 -    ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\\\
  44.107 -$logic$ &=& {\tt(} $logic$ {\tt)} \\
  44.108 -      &$|$& $logic^{(4)}$ {\tt::} $type$ & (3) \\
  44.109 -      &$|$& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$
  44.110 -    ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\
  44.111 -      &$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\
  44.112 -      &$|$& {\tt TYPE} {\tt(} $type$ {\tt)} \\\\
  44.113 -$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
  44.114 -$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
  44.115 -    &$|$& $id$ {\tt ::} $type$ & (0) \\\\
  44.116 -$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\
  44.117 -$pttrn$ &=& $idt$ \\\\
  44.118 -$type$ &=& {\tt(} $type$ {\tt)} \\
  44.119 -     &$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
  44.120 -       ~~$|$~~ $tvar$ {\tt::} $sort$ \\
  44.121 -     &$|$& $id$ ~~$|$~~ $type^{(\infty)}$ $id$
  44.122 -                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
  44.123 -     &$|$& $longid$ ~~$|$~~ $type^{(\infty)}$ $longid$
  44.124 -                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $longid$ \\
  44.125 -     &$|$& $type^{(1)}$ {\tt =>} $type$ & (0) \\
  44.126 -     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0) \\\\
  44.127 -$sort$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ {\tt\ttlbrace\ttrbrace} ~~$|$~~
  44.128 -  {\tt\ttlbrace} $id$ ~$|$~ $longid${\tt,}\dots{\tt,} $id$ ~$|$~$longid$ {\tt\ttrbrace}
  44.129 -\end{tabular}
  44.130 -\index{*PROP symbol}
  44.131 -\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
  44.132 -\index{*:: symbol}\index{*=> symbol}
  44.133 -\index{sort constraints}
  44.134 -%the index command: a percent is permitted, but braces must match!
  44.135 -\index{%@{\tt\%} symbol}
  44.136 -\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
  44.137 -\index{*[ symbol}\index{*] symbol}
  44.138 -\index{*"!"! symbol}
  44.139 -\index{*"["| symbol}
  44.140 -\index{*"|"] symbol}
  44.141 -\end{center}
  44.142 -\caption{Meta-logic syntax}\label{fig:pure_gram}
  44.143 -\end{figure}
  44.144 -
  44.145 -
  44.146 -\section{The Pure syntax} \label{sec:basic_syntax}
  44.147 -\index{syntax!Pure|(}
  44.148 -
  44.149 -At the root of all object-logics lies the theory \thydx{Pure}.  It
  44.150 -contains, among many other things, the Pure syntax.  An informal account of
  44.151 -this basic syntax (types, terms and formulae) appears in
  44.152 -\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}%
  44.153 -{\S\ref{sec:forward}}.  A more precise description using a priority grammar
  44.154 -appears in Fig.\ts\ref{fig:pure_gram}.  It defines the following
  44.155 -nonterminals:
  44.156 -\begin{ttdescription}
  44.157 -  \item[\ndxbold{any}] denotes any term.
  44.158 -
  44.159 -  \item[\ndxbold{prop}] denotes terms of type {\tt prop}.  These are formulae
  44.160 -    of the meta-logic.  Note that user constants of result type {\tt prop}
  44.161 -    (i.e.\ $c :: \ldots \To prop$) should always provide concrete syntax.
  44.162 -    Otherwise atomic propositions with head $c$ may be printed incorrectly.
  44.163 -
  44.164 -  \item[\ndxbold{aprop}] denotes atomic propositions.
  44.165 -
  44.166 -%% FIXME huh!?
  44.167 -%  These typically
  44.168 -%  include the judgement forms of the object-logic; its definition
  44.169 -%  introduces a meta-level predicate for each judgement form.
  44.170 -
  44.171 -  \item[\ndxbold{logic}] denotes terms whose type belongs to class
  44.172 -    \cldx{logic}, excluding type \tydx{prop}.
  44.173 -
  44.174 -  \item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained
  44.175 -    by types.
  44.176 -    
  44.177 -  \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
  44.178 -    abstraction, cases etc.  Initially the same as $idt$ and $idts$,
  44.179 -    these are intended to be augmented by user extensions.
  44.180 -
  44.181 -  \item[\ndxbold{type}] denotes types of the meta-logic.
  44.182 -
  44.183 -  \item[\ndxbold{sort}] denotes meta-level sorts.
  44.184 -\end{ttdescription}
  44.185 -
  44.186 -\begin{warn}
  44.187 -  In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|,
  44.188 -  treating {\tt y} like a type constructor applied to {\tt nat}.  The
  44.189 -  likely result is an error message.  To avoid this interpretation, use
  44.190 -  parentheses and write \verb|(x::nat) y|.
  44.191 -  \index{type constraints}\index{*:: symbol}
  44.192 -
  44.193 -  Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
  44.194 -  yields an error.  The correct form is \verb|(x::nat) (y::nat)|.
  44.195 -\end{warn}
  44.196 -
  44.197 -\begin{warn}
  44.198 -  Type constraints bind very weakly.  For example, \verb!x<y::nat! is normally
  44.199 -  parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 3 or less, in
  44.200 -  which case the string is likely to be ambiguous.  The correct form is
  44.201 -  \verb!x<(y::nat)!.
  44.202 -\end{warn}
  44.203 -
  44.204 -\subsection{Logical types and default syntax}\label{logical-types}
  44.205 -\index{lambda calc@$\lambda$-calculus}
  44.206 -
  44.207 -Isabelle's representation of mathematical languages is based on the
  44.208 -simply typed $\lambda$-calculus.  All logical types, namely those of
  44.209 -class \cldx{logic}, are automatically equipped with a basic syntax of
  44.210 -types, identifiers, variables, parentheses, $\lambda$-abstraction and
  44.211 -application.
  44.212 -\begin{warn}
  44.213 -  Isabelle combines the syntaxes for all types of class \cldx{logic} by
  44.214 -  mapping all those types to the single nonterminal $logic$.  Thus all
  44.215 -  productions of $logic$, in particular $id$, $var$ etc, become available.
  44.216 -\end{warn}
  44.217 -
  44.218 -
  44.219 -\subsection{Lexical matters}
  44.220 -The parser does not process input strings directly.  It operates on token
  44.221 -lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
  44.222 -tokens: \bfindex{delimiters} and \bfindex{name tokens}.
  44.223 -
  44.224 -\index{reserved words}
  44.225 -Delimiters can be regarded as reserved words of the syntax.  You can
  44.226 -add new ones when extending theories.  In Fig.\ts\ref{fig:pure_gram} they
  44.227 -appear in typewriter font, for example {\tt ==}, {\tt =?=} and
  44.228 -{\tt PROP}\@.
  44.229 -
  44.230 -Name tokens have a predefined syntax.  The lexer distinguishes six disjoint
  44.231 -classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
  44.232 -identifiers\index{type identifiers}, type unknowns\index{type unknowns},
  44.233 -\rmindex{numerals}, \rmindex{strings}.  They are denoted by \ndxbold{id},
  44.234 -\ndxbold{var}, \ndxbold{tid}, \ndxbold{tvar}, \ndxbold{num}, \ndxbold{xnum},
  44.235 -\ndxbold{xstr}, respectively.  Typical examples are {\tt x}, {\tt ?x7}, {\tt
  44.236 -  'a}, {\tt ?'a3}, {\tt \#42}, {\tt ''foo bar''}.  Here is the precise syntax:
  44.237 -\begin{eqnarray*}
  44.238 -id        & =   & letter\,quasiletter^* \\
  44.239 -longid    & =   & id (\mbox{\tt .}id)^+ \\
  44.240 -var       & =   & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
  44.241 -tid       & =   & \mbox{\tt '}id \\
  44.242 -tvar      & =   & \mbox{\tt ?}tid ~~|~~
  44.243 -                  \mbox{\tt ?}tid\mbox{\tt .}nat \\
  44.244 -num       & =   & nat ~~|~~ \mbox{\tt-}nat ~~|~~ \verb,0x,\,hex^+ ~~|~~ \verb,0b,\,bin^+ \\
  44.245 -xnum      & =   & \mbox{\tt \#}num \\
  44.246 -xstr      & =   & \mbox{\tt ''~\dots~\tt ''} \\[1ex]
  44.247 -letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~| \\
  44.248 -      &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
  44.249 -quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
  44.250 -latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
  44.251 -digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
  44.252 -nat & = & digit^+ \\
  44.253 -bin & = & \verb,0, ~|~ \verb,1, \\
  44.254 -hex & = & digit  ~|~  \verb,a, ~|~ \dots ~|~ \verb,f, ~|~ \verb,A, ~|~ \dots ~|~ \verb,F, \\
  44.255 -greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
  44.256 -      &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
  44.257 -      &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
  44.258 -      &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
  44.259 -      &   & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
  44.260 -      &   & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
  44.261 -      &   & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
  44.262 -      &   & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
  44.263 -\end{eqnarray*}
  44.264 -The lexer repeatedly takes the longest prefix of the input string that
  44.265 -forms a valid token.  A maximal prefix that is both a delimiter and a
  44.266 -name is treated as a delimiter.  Spaces, tabs, newlines and formfeeds
  44.267 -are separators; they never occur within tokens, except those of class
  44.268 -$xstr$.
  44.269 -
  44.270 -\medskip
  44.271 -Delimiters need not be separated by white space.  For example, if {\tt -}
  44.272 -is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
  44.273 -two consecutive occurrences of the token~{\tt -}.  In contrast, \ML\
  44.274 -treats {\tt --} as a single symbolic name.  The consequence of Isabelle's
  44.275 -more liberal scheme is that the same string may be parsed in different ways
  44.276 -after extending the syntax: after adding {\tt --} as a delimiter, the input
  44.277 -{\tt --} is treated as a single token.
  44.278 -
  44.279 -A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally
  44.280 -a pair of base name and index (\ML\ type \mltydx{indexname}).  These
  44.281 -components are either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
  44.282 -run together as in {\tt ?x1}.  The latter form is possible if the base name
  44.283 -does not end with digits.  If the index is 0, it may be dropped altogether:
  44.284 -{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
  44.285 -
  44.286 -Tokens of class $num$, $xnum$ or $xstr$ are not used by the meta-logic.
  44.287 -Object-logics may provide numerals and string constants by adding appropriate
  44.288 -productions and translation functions.
  44.289 -
  44.290 -\medskip
  44.291 -Although name tokens are returned from the lexer rather than the parser, it
  44.292 -is more logical to regard them as nonterminals.  Delimiters, however, are
  44.293 -terminals; they are just syntactic sugar and contribute nothing to the
  44.294 -abstract syntax tree.
  44.295 -
  44.296 -
  44.297 -\subsection{*Inspecting the syntax} \label{pg:print_syn}
  44.298 -\begin{ttbox}
  44.299 -syn_of              : theory -> Syntax.syntax
  44.300 -print_syntax        : theory -> unit
  44.301 -Syntax.print_syntax : Syntax.syntax -> unit
  44.302 -Syntax.print_gram   : Syntax.syntax -> unit
  44.303 -Syntax.print_trans  : Syntax.syntax -> unit
  44.304 -\end{ttbox}
  44.305 -The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes
  44.306 -in \ML.  You can display values of this type by calling the following
  44.307 -functions:
  44.308 -\begin{ttdescription}
  44.309 -\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
  44.310 -  theory~{\it thy} as an \ML\ value.
  44.311 -
  44.312 -\item[\ttindexbold{print_syntax} $thy$] uses {\tt Syntax.print_syntax}
  44.313 - to display the syntax part of theory $thy$.
  44.314 -
  44.315 -\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
  44.316 -  information contained in the syntax {\it syn}.  The displayed output can
  44.317 -  be large.  The following two functions are more selective.
  44.318 -
  44.319 -\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
  44.320 -  of~{\it syn}, namely the lexicon, logical types and productions.  These are
  44.321 -  discussed below.
  44.322 -
  44.323 -\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
  44.324 -  part of~{\it syn}, namely the constants, parse/print macros and
  44.325 -  parse/print translations.
  44.326 -\end{ttdescription}
  44.327 -
  44.328 -The output of the above print functions is divided into labelled sections.
  44.329 -The grammar is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}.
  44.330 -The rest refers to syntactic translations and macro expansion.  Here is an
  44.331 -explanation of the various sections.
  44.332 -\begin{description}
  44.333 -  \item[{\tt lexicon}] lists the delimiters used for lexical
  44.334 -    analysis.\index{delimiters}
  44.335 -
  44.336 -  \item[{\tt logtypes}] lists the types that are regarded the same as {\tt
  44.337 -    logic} syntactically.  Thus types of object-logics (e.g.\ {\tt nat}, say)
  44.338 -    will be automatically equipped with the standard syntax of
  44.339 -    $\lambda$-calculus.
  44.340 -
  44.341 -  \item[{\tt prods}] lists the \rmindex{productions} of the priority grammar.
  44.342 -    The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
  44.343 -    Each delimiter is quoted.  Some productions are shown with {\tt =>} and
  44.344 -    an attached string.  These strings later become the heads of parse
  44.345 -    trees; they also play a vital role when terms are printed (see
  44.346 -    \S\ref{sec:asts}).
  44.347 -
  44.348 -    Productions with no strings attached are called {\bf copy
  44.349 -      productions}\indexbold{productions!copy}.  Their right-hand side must
  44.350 -    have exactly one nonterminal symbol (or name token).  The parser does
  44.351 -    not create a new parse tree node for copy productions, but simply
  44.352 -    returns the parse tree of the right-hand symbol.
  44.353 -
  44.354 -    If the right-hand side consists of a single nonterminal with no
  44.355 -    delimiters, then the copy production is called a {\bf chain
  44.356 -      production}.  Chain productions act as abbreviations:
  44.357 -    conceptually, they are removed from the grammar by adding new
  44.358 -    productions.  Priority information attached to chain productions is
  44.359 -    ignored; only the dummy value $-1$ is displayed.
  44.360 -    
  44.361 -  \item[\ttindex{print_modes}] lists the alternative print modes
  44.362 -    provided by this syntax (see \S\ref{sec:prmodes}).
  44.363 -
  44.364 -  \item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}]
  44.365 -    relate to macros (see \S\ref{sec:macros}).
  44.366 -
  44.367 -  \item[{\tt parse_ast_translation}, {\tt print_ast_translation}]
  44.368 -    list sets of constants that invoke translation functions for abstract
  44.369 -    syntax trees.  Section \S\ref{sec:asts} below discusses this obscure
  44.370 -    matter.\index{constants!for translations}
  44.371 -
  44.372 -  \item[{\tt parse_translation}, {\tt print_translation}] list the sets
  44.373 -    of constants that invoke translation functions for terms (see
  44.374 -    \S\ref{sec:tr_funs}).
  44.375 -\end{description}
  44.376 -\index{syntax!Pure|)}
  44.377 -
  44.378  
  44.379  \section{Mixfix declarations} \label{sec:mixfix}
  44.380  \index{mixfix declarations|(}
  44.381 @@ -515,49 +144,6 @@
  44.382    syntax}.  Try this as an exercise and study the changes in the
  44.383  grammar.
  44.384  
  44.385 -\subsection{The mixfix template}
  44.386 -Let us now take a closer look at the string $template$ appearing in mixfix
  44.387 -annotations.  This string specifies a list of parsing and printing
  44.388 -directives: delimiters\index{delimiters}, arguments, spaces, blocks of
  44.389 -indentation and line breaks.  These are encoded by the following character
  44.390 -sequences:
  44.391 -\index{pretty printing|(}
  44.392 -\begin{description}
  44.393 -\item[~$d$~] is a delimiter, namely a non-empty sequence of characters
  44.394 -  other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
  44.395 -  Even these characters may appear if escaped; this means preceding it with
  44.396 -  a~{\tt '} (single quote).  Thus you have to write {\tt ''} if you really
  44.397 -  want a single quote.  Furthermore, a~{\tt '} followed by a space separates
  44.398 -  delimiters without extra white space being added for printing.
  44.399 -
  44.400 -\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
  44.401 -  or name token.
  44.402 -
  44.403 -\item[~$s$~] is a non-empty sequence of spaces for printing.  This and the
  44.404 -  following specifications do not affect parsing at all.
  44.405 -
  44.406 -\item[~{\tt(}$n$~] opens a pretty printing block.  The optional number $n$
  44.407 -  specifies how much indentation to add when a line break occurs within the
  44.408 -  block.  If {\tt(} is not followed by digits, the indentation defaults
  44.409 -  to~0.
  44.410 -
  44.411 -\item[~{\tt)}~] closes a pretty printing block.
  44.412 -
  44.413 -\item[~{\tt//}~] forces a line break.
  44.414 -
  44.415 -\item[~{\tt/}$s$~] allows a line break.  Here $s$ stands for the string of
  44.416 -  spaces (zero or more) right after the {\tt /} character.  These spaces
  44.417 -  are printed if the break is not taken.
  44.418 -\end{description}
  44.419 -For example, the template {\tt"(_ +/ _)"} specifies an infix operator.
  44.420 -There are two argument positions; the delimiter~{\tt+} is preceded by a
  44.421 -space and followed by a space or line break; the entire phrase is a pretty
  44.422 -printing block.  Other examples appear in Fig.\ts\ref{fig:set_trans} below.
  44.423 -Isabelle's pretty printer resembles the one described in
  44.424 -Paulson~\cite{paulson-ml2}.
  44.425 -
  44.426 -\index{pretty printing|)}
  44.427 -
  44.428  
  44.429  \subsection{Infixes}
  44.430  \indexbold{infixes}
  44.431 @@ -723,141 +309,6 @@
  44.432  ambiguity should be eliminated by changing the grammar or the rule.
  44.433  
  44.434  
  44.435 -\section{Example: some minimal logics} \label{sec:min_logics}
  44.436 -\index{examples!of logic definitions}
  44.437 -
  44.438 -This section presents some examples that have a simple syntax.  They
  44.439 -demonstrate how to define new object-logics from scratch.
  44.440 -
  44.441 -First we must define how an object-logic syntax is embedded into the
  44.442 -meta-logic.  Since all theorems must conform to the syntax for~\ndx{prop}
  44.443 -(see Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
  44.444 -object-level syntax.  Assume that the syntax of your object-logic defines a
  44.445 -meta-type~\tydx{o} of formulae which refers to the nonterminal {\tt logic}.
  44.446 -These formulae can now appear in axioms and theorems wherever \ndx{prop} does
  44.447 -if you add the production
  44.448 -\[ prop ~=~ logic. \]
  44.449 -This is not supposed to be a copy production but an implicit coercion from
  44.450 -formulae to propositions:
  44.451 -\begin{ttbox}
  44.452 -Base = Pure +
  44.453 -types
  44.454 -  o
  44.455 -arities
  44.456 -  o :: logic
  44.457 -consts
  44.458 -  Trueprop :: o => prop   ("_" 5)
  44.459 -end
  44.460 -\end{ttbox}
  44.461 -The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
  44.462 -coercion function.  Assuming this definition resides in a file {\tt Base.thy},
  44.463 -you have to load it with the command {\tt use_thy "Base"}.
  44.464 -
  44.465 -One of the simplest nontrivial logics is {\bf minimal logic} of
  44.466 -implication.  Its definition in Isabelle needs no advanced features but
  44.467 -illustrates the overall mechanism nicely:
  44.468 -\begin{ttbox}
  44.469 -Hilbert = Base +
  44.470 -consts
  44.471 -  "-->" :: [o, o] => o   (infixr 10)
  44.472 -rules
  44.473 -  K     "P --> Q --> P"
  44.474 -  S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
  44.475 -  MP    "[| P --> Q; P |] ==> Q"
  44.476 -end
  44.477 -\end{ttbox}
  44.478 -After loading this definition from the file {\tt Hilbert.thy}, you can
  44.479 -start to prove theorems in the logic:
  44.480 -\begin{ttbox}
  44.481 -Goal "P --> P";
  44.482 -{\out Level 0}
  44.483 -{\out P --> P}
  44.484 -{\out  1.  P --> P}
  44.485 -\ttbreak
  44.486 -by (resolve_tac [Hilbert.MP] 1);
  44.487 -{\out Level 1}
  44.488 -{\out P --> P}
  44.489 -{\out  1.  ?P --> P --> P}
  44.490 -{\out  2.  ?P}
  44.491 -\ttbreak
  44.492 -by (resolve_tac [Hilbert.MP] 1);
  44.493 -{\out Level 2}
  44.494 -{\out P --> P}
  44.495 -{\out  1.  ?P1 --> ?P --> P --> P}
  44.496 -{\out  2.  ?P1}
  44.497 -{\out  3.  ?P}
  44.498 -\ttbreak
  44.499 -by (resolve_tac [Hilbert.S] 1);
  44.500 -{\out Level 3}
  44.501 -{\out P --> P}
  44.502 -{\out  1.  P --> ?Q2 --> P}
  44.503 -{\out  2.  P --> ?Q2}
  44.504 -\ttbreak
  44.505 -by (resolve_tac [Hilbert.K] 1);
  44.506 -{\out Level 4}
  44.507 -{\out P --> P}
  44.508 -{\out  1.  P --> ?Q2}
  44.509 -\ttbreak
  44.510 -by (resolve_tac [Hilbert.K] 1);
  44.511 -{\out Level 5}
  44.512 -{\out P --> P}
  44.513 -{\out No subgoals!}
  44.514 -\end{ttbox}
  44.515 -As we can see, this Hilbert-style formulation of minimal logic is easy to
  44.516 -define but difficult to use.  The following natural deduction formulation is
  44.517 -better:
  44.518 -\begin{ttbox}
  44.519 -MinI = Base +
  44.520 -consts
  44.521 -  "-->" :: [o, o] => o   (infixr 10)
  44.522 -rules
  44.523 -  impI  "(P ==> Q) ==> P --> Q"
  44.524 -  impE  "[| P --> Q; P |] ==> Q"
  44.525 -end
  44.526 -\end{ttbox}
  44.527 -Note, however, that although the two systems are equivalent, this fact
  44.528 -cannot be proved within Isabelle.  Axioms {\tt S} and {\tt K} can be
  44.529 -derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
  44.530 -  Hilbert}.  The reason is that {\tt impI} is only an {\bf admissible} rule
  44.531 -in {\tt Hilbert}, something that can only be shown by induction over all
  44.532 -possible proofs in {\tt Hilbert}.
  44.533 -
  44.534 -We may easily extend minimal logic with falsity:
  44.535 -\begin{ttbox}
  44.536 -MinIF = MinI +
  44.537 -consts
  44.538 -  False :: o
  44.539 -rules
  44.540 -  FalseE "False ==> P"
  44.541 -end
  44.542 -\end{ttbox}
  44.543 -On the other hand, we may wish to introduce conjunction only:
  44.544 -\begin{ttbox}
  44.545 -MinC = Base +
  44.546 -consts
  44.547 -  "&" :: [o, o] => o   (infixr 30)
  44.548 -\ttbreak
  44.549 -rules
  44.550 -  conjI  "[| P; Q |] ==> P & Q"
  44.551 -  conjE1 "P & Q ==> P"
  44.552 -  conjE2 "P & Q ==> Q"
  44.553 -end
  44.554 -\end{ttbox}
  44.555 -And if we want to have all three connectives together, we create and load a
  44.556 -theory file consisting of a single line:
  44.557 -\begin{ttbox}
  44.558 -MinIFC = MinIF + MinC
  44.559 -\end{ttbox}
  44.560 -Now we can prove mixed theorems like
  44.561 -\begin{ttbox}
  44.562 -Goal "P & False --> Q";
  44.563 -by (resolve_tac [MinI.impI] 1);
  44.564 -by (dresolve_tac [MinC.conjE2] 1);
  44.565 -by (eresolve_tac [MinIF.FalseE] 1);
  44.566 -\end{ttbox}
  44.567 -Try this as an exercise!
  44.568 -
  44.569 -
  44.570  %%% Local Variables: 
  44.571  %%% mode: latex
  44.572  %%% TeX-master: "ref"