# HG changeset patch
# User wenzelm
# Date 1210368017 -7200
# Node ID 3cff7b336c75ce597479e4ccb01c025b849f87a9
# Parent  a3afbb414b69474232ab23204ed2b28f98ca55e8
proper antiquotations for commands;

diff -r a3afbb414b69 -r 3cff7b336c75 doc-src/IsarRef/Thy/pure.thy
--- a/doc-src/IsarRef/Thy/pure.thy	Fri May 09 23:19:49 2008 +0200
+++ b/doc-src/IsarRef/Thy/pure.thy	Fri May 09 23:20:17 2008 +0200
@@ -908,14 +908,14 @@
 
 text {*
   \begin{matharray}{rcl}
-    \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
-    \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
-    \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
-    \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
-    \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
-    \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
-    \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
-    \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
+    @{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+    @{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+    @{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+    @{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+    @{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+    @{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
+    @{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
+    @{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   \end{matharray}
 
   From a theory context, proof mode is entered by an initial goal
@@ -1439,12 +1439,12 @@
   be used in scripts, too.
 
   \begin{matharray}{rcl}
-    @{command_def "apply"}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
-    @{command_def "apply_end"}^* & : & \isartrans{proof(state)}{proof(state)} \\
-    @{command_def "done"}^* & : & \isartrans{proof(prove)}{proof(state)} \\
-    @{command_def "defer"}^* & : & \isartrans{proof}{proof} \\
-    @{command_def "prefer"}^* & : & \isartrans{proof}{proof} \\
-    @{command_def "back"}^* & : & \isartrans{proof}{proof} \\
+    @{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
+    @{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
+    @{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
+    @{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
+    @{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
+    @{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
   \end{matharray}
 
   \begin{rail}
@@ -1539,13 +1539,13 @@
 
 text {*
   \begin{matharray}{rcl}
-    \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
-    \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
-    \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
-    \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
-    \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
-    \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
-    \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
+    @{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+    @{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   \end{matharray}
 
   These diagnostic commands assist interactive development.  Note that
@@ -1628,16 +1628,16 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "print_commands"}^* & : & \isarkeep{\cdot} \\
-    @{command_def "print_theory"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "print_syntax"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "print_methods"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "print_attributes"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "print_theorems"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "find_theorems"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "thms_deps"}^* & : & \isarkeep{theory~|~proof} \\
-    @{command_def "print_facts"}^* & : & \isarkeep{proof} \\
-    @{command_def "print_binds"}^* & : & \isarkeep{proof} \\
+    @{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+    @{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "thms_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+    @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
+    @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
   \end{matharray}
 
   \begin{rail}
@@ -1747,11 +1747,11 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "cd"}^* & : & \isarkeep{\cdot} \\
-    @{command_def "pwd"}^* & : & \isarkeep{\cdot} \\
-    @{command_def "use_thy"}^* & : & \isarkeep{\cdot} \\
-    @{command_def "display_drafts"}^* & : & \isarkeep{\cdot} \\
-    @{command_def "print_drafts"}^* & : & \isarkeep{\cdot} \\
+    @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+    @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+    @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+    @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+    @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
   \end{matharray}
 
   \begin{rail}