diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Nov 13 21:45:40 2008 +0100
@@ -10,8 +10,8 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOL) "typedecl"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "typedef"} & : & \isartrans{theory}{proof(prove)} \\
+    @{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
   \begin{rail}
@@ -79,7 +79,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & \isaratt \\
+    @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
@@ -185,7 +185,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOL) "record"} & : & \isartrans{theory}{theory} \\
+    @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   \begin{rail}
@@ -359,8 +359,8 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\
-  @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{proof} \\
+    @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
+  @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
   \begin{rail}
@@ -403,10 +403,10 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOL) "primrec"} & : & \isarkeep{local{\dsh}theory} \\
-    @{command_def (HOL) "fun"} & : & \isarkeep{local{\dsh}theory} \\
-    @{command_def (HOL) "function"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
-    @{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+    @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+    @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
   \begin{rail}
@@ -509,9 +509,9 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{method_def (HOL) pat_completeness} & : & \isarmeth \\
-    @{method_def (HOL) relation} & : & \isarmeth \\
-    @{method_def (HOL) lexicographic_order} & : & \isarmeth \\
+    @{method_def (HOL) pat_completeness} & : & @{text method} \\
+    @{method_def (HOL) relation} & : & @{text method} \\
+    @{method_def (HOL) lexicographic_order} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
@@ -558,8 +558,8 @@
   (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
 
   \begin{matharray}{rcl}
-    @{command_def (HOL) "recdef"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & \isartrans{theory}{proof(prove)} \\
+    @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
+    @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
   \begin{rail}
@@ -602,9 +602,9 @@
   globally, using the following attributes.
 
   \begin{matharray}{rcl}
-    @{attribute_def (HOL) recdef_simp} & : & \isaratt \\
-    @{attribute_def (HOL) recdef_cong} & : & \isaratt \\
-    @{attribute_def (HOL) recdef_wf} & : & \isaratt \\
+    @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\
+    @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\
+    @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
@@ -640,11 +640,11 @@
   to use inference rules for type-checking.
 
   \begin{matharray}{rcl}
-    @{command_def (HOL) "inductive"} & : & \isarkeep{local{\dsh}theory} \\
-    @{command_def (HOL) "inductive_set"} & : & \isarkeep{local{\dsh}theory} \\
-    @{command_def (HOL) "coinductive"} & : & \isarkeep{local{\dsh}theory} \\
-    @{command_def (HOL) "coinductive_set"} & : & \isarkeep{local{\dsh}theory} \\
-    @{attribute_def (HOL) mono} & : & \isaratt \\
+    @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{attribute_def (HOL) mono} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
@@ -757,8 +757,8 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{method_def (HOL) arith} & : & \isarmeth \\
-    @{attribute_def (HOL) arith_split} & : & \isaratt \\
+    @{method_def (HOL) arith} & : & @{text method} \\
+    @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
   \end{matharray}
 
   The @{method (HOL) arith} method decides linear arithmetic problems
@@ -800,11 +800,11 @@
   search over and over again.
 
   \begin{matharray}{rcl}
-    @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
-    @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
-    @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
-    @{method_def (HOL) metis} & : & \isarmeth \\
+    @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+    @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+    @{method_def (HOL) metis} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
@@ -864,10 +864,10 @@
   \secref{sec:cases-induct} for proper Isar versions of similar ideas.
 
   \begin{matharray}{rcl}
-    @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
-    @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
-    @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
-    @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & \isartrans{theory}{theory} \\
+    @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
+    @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
+    @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
+    @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   \begin{rail}
@@ -929,12 +929,12 @@
   (this actually covers the new-style theory format as well).
 
   \begin{matharray}{rcl}
-    @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{command_def (HOL) "code_module"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_library"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "consts_code"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "types_code"} & : & \isartrans{theory}{theory} \\  
-    @{attribute_def (HOL) code} & : & \isaratt \\
+    @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\  
+    @{attribute_def (HOL) code} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
@@ -991,21 +991,21 @@
   introduction on how to use it.
 
   \begin{matharray}{rcl}
-    @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{command_def (HOL) "code_datatype"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_const"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_type"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_class"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_instance"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_monad"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "code_abort"} & : & \isartrans{theory}{theory} \\
-    @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{attribute_def (HOL) code} & : & \isaratt \\
+    @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{attribute_def (HOL) code} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
@@ -1179,8 +1179,8 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\
-    @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\
+    @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+    @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
   \begin{rail}