1.1 --- a/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:43:46 2008 +0100
1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:45:40 2008 +0100
1.3 @@ -10,8 +10,8 @@
1.4
1.5 text {*
1.6 \begin{matharray}{rcl}
1.7 - @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
1.8 - @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\
1.9 + @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
1.10 + @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
1.11 \end{matharray}
1.12
1.13 Isabelle/Isar theories are defined via theory files, which may
1.14 @@ -82,8 +82,8 @@
1.15 global theory context.
1.16
1.17 \begin{matharray}{rcll}
1.18 - @{command_def "context"} & : & \isartrans{theory}{local{\dsh}theory} \\
1.19 - @{command_def (local) "end"} & : & \isartrans{local{\dsh}theory}{theory} \\
1.20 + @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
1.21 + @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
1.22 \end{matharray}
1.23
1.24 \indexouternonterm{target}
1.25 @@ -143,13 +143,13 @@
1.26
1.27 text {*
1.28 \begin{matharray}{rcll}
1.29 - @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\
1.30 - @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\
1.31 - @{attribute_def "defn"} & : & \isaratt \\
1.32 - @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\
1.33 - @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.34 - @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\
1.35 - @{command_def "no_notation"} & : & \isarkeep{local{\dsh}theory} \\
1.36 + @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
1.37 + @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.38 + @{attribute_def "defn"} & : & @{text attribute} \\
1.39 + @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.40 + @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
1.41 + @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.42 + @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.43 \end{matharray}
1.44
1.45 These specification mechanisms provide a slightly more abstract view
1.46 @@ -253,8 +253,8 @@
1.47 means of an attribute.
1.48
1.49 \begin{matharray}{rcl}
1.50 - @{command_def "declaration"} & : & \isarkeep{local{\dsh}theory} \\
1.51 - @{command_def "declare"} & : & \isarkeep{local{\dsh}theory} \\
1.52 + @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.53 + @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.54 \end{matharray}
1.55
1.56 \begin{rail}
1.57 @@ -295,11 +295,11 @@
1.58
1.59 text {*
1.60 \begin{matharray}{rcl}
1.61 - @{command_def "locale"} & : & \isartrans{theory}{local{\dsh}theory} \\
1.62 - @{command_def "print_locale"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.63 - @{command_def "print_locales"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.64 - @{method_def intro_locales} & : & \isarmeth \\
1.65 - @{method_def unfold_locales} & : & \isarmeth \\
1.66 + @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
1.67 + @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.68 + @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.69 + @{method_def intro_locales} & : & @{text method} \\
1.70 + @{method_def unfold_locales} & : & @{text method} \\
1.71 \end{matharray}
1.72
1.73 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
1.74 @@ -461,9 +461,9 @@
1.75 "interpret"}).
1.76
1.77 \begin{matharray}{rcl}
1.78 - @{command_def "interpretation"} & : & \isartrans{theory}{proof(prove)} \\
1.79 - @{command_def "interpret"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
1.80 - @{command_def "print_interps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.81 + @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
1.82 + @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
1.83 + @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.84 \end{matharray}
1.85
1.86 \indexouternonterm{interp}
1.87 @@ -601,12 +601,12 @@
1.88 tutorial.
1.89
1.90 \begin{matharray}{rcl}
1.91 - @{command_def "class"} & : & \isartrans{theory}{local{\dsh}theory} \\
1.92 - @{command_def "instantiation"} & : & \isartrans{theory}{local{\dsh}theory} \\
1.93 - @{command_def "instance"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
1.94 - @{command_def "subclass"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
1.95 - @{command_def "print_classes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.96 - @{method_def intro_classes} & : & \isarmeth \\
1.97 + @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
1.98 + @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
1.99 + @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.100 + @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.101 + @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.102 + @{method_def intro_classes} & : & @{text method} \\
1.103 \end{matharray}
1.104
1.105 \begin{rail}
1.106 @@ -716,8 +716,8 @@
1.107
1.108 text {*
1.109 \begin{matharray}{rcl}
1.110 - @{command_def "axclass"} & : & \isartrans{theory}{theory} \\
1.111 - @{command_def "instance"} & : & \isartrans{theory}{proof(prove)} \\
1.112 + @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
1.113 + @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
1.114 \end{matharray}
1.115
1.116 Axiomatic type classes are Isabelle/Pure's primitive
1.117 @@ -772,7 +772,7 @@
1.118 end-users.
1.119
1.120 \begin{matharray}{rcl}
1.121 - @{command_def "overloading"} & : & \isartrans{theory}{local{\dsh}theory} \\
1.122 + @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
1.123 \end{matharray}
1.124
1.125 \begin{rail}
1.126 @@ -805,12 +805,12 @@
1.127
1.128 text {*
1.129 \begin{matharray}{rcl}
1.130 - @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
1.131 - @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
1.132 - @{command_def "ML_prf"} & : & \isarkeep{proof} \\
1.133 - @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
1.134 - @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
1.135 - @{command_def "setup"} & : & \isartrans{theory}{theory} \\
1.136 + @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.137 + @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.138 + @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
1.139 + @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
1.140 + @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
1.141 + @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
1.142 \end{matharray}
1.143
1.144 \begin{mldecls}
1.145 @@ -879,10 +879,10 @@
1.146
1.147 text {*
1.148 \begin{matharray}{rcll}
1.149 - @{command_def "classes"} & : & \isartrans{theory}{theory} \\
1.150 - @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1.151 - @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
1.152 - @{command_def "class_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.153 + @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
1.154 + @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1.155 + @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
1.156 + @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.157 \end{matharray}
1.158
1.159 \begin{rail}
1.160 @@ -922,10 +922,10 @@
1.161
1.162 text {*
1.163 \begin{matharray}{rcll}
1.164 - @{command_def "types"} & : & \isartrans{theory}{theory} \\
1.165 - @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
1.166 - @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
1.167 - @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1.168 + @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
1.169 + @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
1.170 + @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
1.171 + @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1.172 \end{matharray}
1.173
1.174 \begin{rail}
1.175 @@ -1011,9 +1011,9 @@
1.176 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1.177
1.178 \begin{matharray}{rcl}
1.179 - @{command_def "consts"} & : & \isartrans{theory}{theory} \\
1.180 - @{command_def "defs"} & : & \isartrans{theory}{theory} \\
1.181 - @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
1.182 + @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
1.183 + @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
1.184 + @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
1.185 \end{matharray}
1.186
1.187 \begin{rail}
1.188 @@ -1082,9 +1082,9 @@
1.189
1.190 text {*
1.191 \begin{matharray}{rcll}
1.192 - @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1.193 - @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
1.194 - @{command_def "theorems"} & : & \isarkeep{local{\dsh}theory} \\
1.195 + @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1.196 + @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.197 + @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.198 \end{matharray}
1.199
1.200 \begin{rail}
1.201 @@ -1135,7 +1135,7 @@
1.202 presumed theorems depend on unproven suppositions.
1.203
1.204 \begin{matharray}{rcl}
1.205 - @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
1.206 + @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
1.207 \end{matharray}
1.208
1.209 \begin{rail}
1.210 @@ -1164,9 +1164,9 @@
1.211
1.212 text {*
1.213 \begin{matharray}{rcl}
1.214 - @{command_def "global"} & : & \isartrans{theory}{theory} \\
1.215 - @{command_def "local"} & : & \isartrans{theory}{theory} \\
1.216 - @{command_def "hide"} & : & \isartrans{theory}{theory} \\
1.217 + @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
1.218 + @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
1.219 + @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
1.220 \end{matharray}
1.221
1.222 \begin{rail}
1.223 @@ -1211,10 +1211,10 @@
1.224
1.225 text {*
1.226 \begin{matharray}{rcl}
1.227 - @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
1.228 - @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
1.229 - @{command_def "translations"} & : & \isartrans{theory}{theory} \\
1.230 - @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
1.231 + @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
1.232 + @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
1.233 + @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
1.234 + @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
1.235 \end{matharray}
1.236
1.237 \begin{rail}
1.238 @@ -1262,11 +1262,11 @@
1.239
1.240 text {*
1.241 \begin{matharray}{rcl}
1.242 - @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
1.243 - @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
1.244 - @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
1.245 - @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
1.246 - @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
1.247 + @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
1.248 + @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
1.249 + @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
1.250 + @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
1.251 + @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
1.252 \end{matharray}
1.253
1.254 \begin{rail}