--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:45:40 2008 +0100
@@ -58,18 +58,18 @@
text {*
\begin{matharray}{rcl}
- @{command_def "header"} & : & \isarkeep{toplevel} \\[0.5ex]
- @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\[0.5ex]
- @{command_def "sect"} & : & \isartrans{proof}{proof} \\
- @{command_def "subsect"} & : & \isartrans{proof}{proof} \\
- @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
- @{command_def "txt"} & : & \isartrans{proof}{proof} \\
- @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
+ @{command_def "header"} & : & @{text "toplevel \<rightarrow> toplevel"} \\[0.5ex]
+ @{command_def "chapter"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "section"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "subsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "subsubsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
+ @{command_def "sect"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "subsect"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "subsubsect"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> proof"} \\
\end{matharray}
Markup commands provide a structured way to insert text into the
@@ -138,25 +138,25 @@
text {*
\begin{matharray}{rcl}
- @{antiquotation_def "theory"} & : & \isarantiq \\
- @{antiquotation_def "thm"} & : & \isarantiq \\
- @{antiquotation_def "lemma"} & : & \isarantiq \\
- @{antiquotation_def "prop"} & : & \isarantiq \\
- @{antiquotation_def "term"} & : & \isarantiq \\
- @{antiquotation_def const} & : & \isarantiq \\
- @{antiquotation_def abbrev} & : & \isarantiq \\
- @{antiquotation_def typeof} & : & \isarantiq \\
- @{antiquotation_def typ} & : & \isarantiq \\
- @{antiquotation_def thm_style} & : & \isarantiq \\
- @{antiquotation_def term_style} & : & \isarantiq \\
- @{antiquotation_def "text"} & : & \isarantiq \\
- @{antiquotation_def goals} & : & \isarantiq \\
- @{antiquotation_def subgoals} & : & \isarantiq \\
- @{antiquotation_def prf} & : & \isarantiq \\
- @{antiquotation_def full_prf} & : & \isarantiq \\
- @{antiquotation_def ML} & : & \isarantiq \\
- @{antiquotation_def ML_type} & : & \isarantiq \\
- @{antiquotation_def ML_struct} & : & \isarantiq \\
+ @{antiquotation_def "theory"} & : & @{text antiquotation} \\
+ @{antiquotation_def "thm"} & : & @{text antiquotation} \\
+ @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
+ @{antiquotation_def "prop"} & : & @{text antiquotation} \\
+ @{antiquotation_def "term"} & : & @{text antiquotation} \\
+ @{antiquotation_def const} & : & @{text antiquotation} \\
+ @{antiquotation_def abbrev} & : & @{text antiquotation} \\
+ @{antiquotation_def typeof} & : & @{text antiquotation} \\
+ @{antiquotation_def typ} & : & @{text antiquotation} \\
+ @{antiquotation_def thm_style} & : & @{text antiquotation} \\
+ @{antiquotation_def term_style} & : & @{text antiquotation} \\
+ @{antiquotation_def "text"} & : & @{text antiquotation} \\
+ @{antiquotation_def goals} & : & @{text antiquotation} \\
+ @{antiquotation_def subgoals} & : & @{text antiquotation} \\
+ @{antiquotation_def prf} & : & @{text antiquotation} \\
+ @{antiquotation_def full_prf} & : & @{text antiquotation} \\
+ @{antiquotation_def ML} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_type} & : & @{text antiquotation} \\
+ @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
\end{matharray}
The overall content of an Isabelle/Isar theory may alternate between
@@ -452,8 +452,8 @@
text {*
\begin{matharray}{rcl}
- @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
- @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/Generic.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Thu Nov 13 21:45:40 2008 +0100
@@ -25,7 +25,7 @@
``global'', which may not be changed within a local context.
\begin{matharray}{rcll}
- @{command_def "print_configs"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
\begin{rail}
@@ -52,14 +52,14 @@
text {*
\begin{matharray}{rcl}
- @{method_def unfold} & : & \isarmeth \\
- @{method_def fold} & : & \isarmeth \\
- @{method_def insert} & : & \isarmeth \\[0.5ex]
- @{method_def erule}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def drule}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def frule}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def succeed} & : & \isarmeth \\
- @{method_def fail} & : & \isarmeth \\
+ @{method_def unfold} & : & @{text method} \\
+ @{method_def fold} & : & @{text method} \\
+ @{method_def insert} & : & @{text method} \\[0.5ex]
+ @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def succeed} & : & @{text method} \\
+ @{method_def fail} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -107,16 +107,16 @@
\end{description}
\begin{matharray}{rcl}
- @{attribute_def tagged} & : & \isaratt \\
- @{attribute_def untagged} & : & \isaratt \\[0.5ex]
- @{attribute_def THEN} & : & \isaratt \\
- @{attribute_def COMP} & : & \isaratt \\[0.5ex]
- @{attribute_def unfolded} & : & \isaratt \\
- @{attribute_def folded} & : & \isaratt \\[0.5ex]
- @{attribute_def rotated} & : & \isaratt \\
- @{attribute_def (Pure) elim_format} & : & \isaratt \\
- @{attribute_def standard}@{text "\<^sup>*"} & : & \isaratt \\
- @{attribute_def no_vars}@{text "\<^sup>*"} & : & \isaratt \\
+ @{attribute_def tagged} & : & @{text attribute} \\
+ @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
+ @{attribute_def THEN} & : & @{text attribute} \\
+ @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
+ @{attribute_def unfolded} & : & @{text attribute} \\
+ @{attribute_def folded} & : & @{text attribute} \\[0.5ex]
+ @{attribute_def rotated} & : & @{text attribute} \\
+ @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
+ @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
+ @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -144,8 +144,9 @@
compose rules by resolution. @{attribute THEN} resolves with the
first premise of @{text a} (an alternative position may be also
specified); the @{attribute COMP} version skips the automatic
- lifting process that is normally intended (cf.\ @{ML "op RS"} and
- @{ML "op COMP"} in \cite[\S5]{isabelle-ref}).
+ lifting process that is normally intended (cf.\ @{ML [source=false]
+ "op RS"} and @{ML [source=false] "op COMP"} in
+ \cite[\S5]{isabelle-ref}).
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
@@ -177,9 +178,9 @@
text {*
\begin{matharray}{rcl}
- @{method_def subst} & : & \isarmeth \\
- @{method_def hypsubst} & : & \isarmeth \\
- @{method_def split} & : & \isarmeth \\
+ @{method_def subst} & : & @{text method} \\
+ @{method_def hypsubst} & : & @{text method} \\
+ @{method_def split} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -272,17 +273,17 @@
\secref{sec:pure-meth-att}).
\begin{matharray}{rcl}
- @{method_def rule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def erule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def drule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def frule_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def cut_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def thin_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def subgoal_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def rename_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def rotate_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def tactic}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def raw_tactic}@{text "\<^sup>*"} & : & \isarmeth \\
+ @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -360,8 +361,8 @@
text {*
\begin{matharray}{rcl}
- @{method_def simp} & : & \isarmeth \\
- @{method_def simp_all} & : & \isarmeth \\
+ @{method_def simp} & : & @{text method} \\
+ @{method_def simp_all} & : & @{text method} \\
\end{matharray}
\indexouternonterm{simpmod}
@@ -439,10 +440,10 @@
text {*
\begin{matharray}{rcl}
- @{command_def "print_simpset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{attribute_def simp} & : & \isaratt \\
- @{attribute_def cong} & : & \isaratt \\
- @{attribute_def split} & : & \isaratt \\
+ @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def simp} & : & @{text attribute} \\
+ @{attribute_def cong} & : & @{text attribute} \\
+ @{attribute_def split} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -470,8 +471,8 @@
text {*
\begin{matharray}{rcl}
- @{command_def "simproc_setup"} & : & \isarkeep{local{\dsh}theory} \\
- simproc & : & \isaratt \\
+ @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ simproc & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -516,7 +517,7 @@
text {*
\begin{matharray}{rcl}
- @{attribute_def simplified} & : & \isaratt \\
+ @{attribute_def simplified} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -552,10 +553,10 @@
text {*
\begin{matharray}{rcl}
- @{method_def rule} & : & \isarmeth \\
- @{method_def contradiction} & : & \isarmeth \\
- @{method_def intro} & : & \isarmeth \\
- @{method_def elim} & : & \isarmeth \\
+ @{method_def rule} & : & @{text method} \\
+ @{method_def contradiction} & : & @{text method} \\
+ @{method_def intro} & : & @{text method} \\
+ @{method_def elim} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -595,12 +596,12 @@
text {*
\begin{matharray}{rcl}
- @{method_def blast} & : & \isarmeth \\
- @{method_def fast} & : & \isarmeth \\
- @{method_def slow} & : & \isarmeth \\
- @{method_def best} & : & \isarmeth \\
- @{method_def safe} & : & \isarmeth \\
- @{method_def clarify} & : & \isarmeth \\
+ @{method_def blast} & : & @{text method} \\
+ @{method_def fast} & : & @{text method} \\
+ @{method_def slow} & : & @{text method} \\
+ @{method_def best} & : & @{text method} \\
+ @{method_def safe} & : & @{text method} \\
+ @{method_def clarify} & : & @{text method} \\
\end{matharray}
\indexouternonterm{clamod}
@@ -641,12 +642,12 @@
text {*
\begin{matharray}{rcl}
- @{method_def auto} & : & \isarmeth \\
- @{method_def force} & : & \isarmeth \\
- @{method_def clarsimp} & : & \isarmeth \\
- @{method_def fastsimp} & : & \isarmeth \\
- @{method_def slowsimp} & : & \isarmeth \\
- @{method_def bestsimp} & : & \isarmeth \\
+ @{method_def auto} & : & @{text method} \\
+ @{method_def force} & : & @{text method} \\
+ @{method_def clarsimp} & : & @{text method} \\
+ @{method_def fastsimp} & : & @{text method} \\
+ @{method_def slowsimp} & : & @{text method} \\
+ @{method_def bestsimp} & : & @{text method} \\
\end{matharray}
\indexouternonterm{clasimpmod}
@@ -687,12 +688,12 @@
text {*
\begin{matharray}{rcl}
- @{command_def "print_claset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{attribute_def intro} & : & \isaratt \\
- @{attribute_def elim} & : & \isaratt \\
- @{attribute_def dest} & : & \isaratt \\
- @{attribute_def rule} & : & \isaratt \\
- @{attribute_def iff} & : & \isaratt \\
+ @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def intro} & : & @{text attribute} \\
+ @{attribute_def elim} & : & @{text attribute} \\
+ @{attribute_def dest} & : & @{text attribute} \\
+ @{attribute_def rule} & : & @{text attribute} \\
+ @{attribute_def iff} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -743,7 +744,7 @@
text {*
\begin{matharray}{rcl}
- @{attribute_def swapped} & : & \isaratt \\
+ @{attribute_def swapped} & : & @{text attribute} \\
\end{matharray}
\begin{description}
@@ -760,11 +761,11 @@
text {*
\begin{matharray}{rcl}
- @{command_def "judgment"} & : & \isartrans{theory}{theory} \\
- @{method_def atomize} & : & \isarmeth \\
- @{attribute_def atomize} & : & \isaratt \\
- @{attribute_def rule_format} & : & \isaratt \\
- @{attribute_def rulify} & : & \isaratt \\
+ @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{method_def atomize} & : & @{text method} \\
+ @{attribute_def atomize} & : & @{text attribute} \\
+ @{attribute_def rule_format} & : & @{text attribute} \\
+ @{attribute_def rulify} & : & @{text attribute} \\
\end{matharray}
The very starting point for any Isabelle object-logic is a ``truth
--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy Thu Nov 13 21:45:40 2008 +0100
@@ -10,7 +10,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def (HOLCF) "consts"} & : & \isartrans{theory}{theory} \\
+ @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
@@ -33,7 +33,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\
+ @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
--- 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}
--- a/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:45:40 2008 +0100
@@ -10,13 +10,13 @@
text {*
\begin{matharray}{rcl}
- @{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} \\
+ @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
These diagnostic commands assist interactive development. Note that
@@ -99,16 +99,16 @@
text {*
\begin{matharray}{rcl}
- @{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 "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
- @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
+ @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
\begin{rail}
@@ -190,9 +190,9 @@
text {*
\begin{matharray}{rcl}
- @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
- @{command_def "linear_undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
- @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ @{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
+ @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
+ @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
\end{matharray}
The Isabelle/Isar top-level maintains a two-stage history, for
@@ -219,9 +219,9 @@
text {*
\begin{matharray}{rcl}
- @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
- @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
- @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/Proof.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Thu Nov 13 21:45:40 2008 +0100
@@ -48,9 +48,9 @@
text {*
\begin{matharray}{rcl}
- @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
\end{matharray}
While Isar is inherently block-structured, opening and closing
@@ -90,7 +90,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def "oops"} & : & \isartrans{proof}{theory} \\
+ @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\
\end{matharray}
The @{command "oops"} command discontinues the current proof
@@ -123,10 +123,10 @@
text {*
\begin{matharray}{rcl}
- @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
\end{matharray}
The logical proof context consists of fixed variables and
@@ -208,7 +208,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
@{keyword_def "is"} & : & syntax \\
\end{matharray}
@@ -276,12 +276,12 @@
text {*
\begin{matharray}{rcl}
- @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
- @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
- @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
- @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
- @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
+ @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
+ @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
+ @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
+ @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+ @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
\end{matharray}
New facts are established either by assumption or proof of local
@@ -361,14 +361,14 @@
text {*
\begin{matharray}{rcl}
- @{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} \\
+ @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
+ @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
+ @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
+ @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
+ @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
From a theory context, proof mode is entered by an initial goal
@@ -560,12 +560,12 @@
text {*
\begin{matharray}{rcl}
- @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
- @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
- @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
- @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
- @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
- @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\
+ @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
\end{matharray}
Arbitrary goal refinement via tactics is considered harmful.
@@ -676,19 +676,19 @@
\chref{ch:gen-tools} and \chref{ch:hol}).
\begin{matharray}{rcl}
- @{method_def "-"} & : & \isarmeth \\
- @{method_def "fact"} & : & \isarmeth \\
- @{method_def "assumption"} & : & \isarmeth \\
- @{method_def "this"} & : & \isarmeth \\
- @{method_def "rule"} & : & \isarmeth \\
- @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
- @{attribute_def (Pure) "intro"} & : & \isaratt \\
- @{attribute_def (Pure) "elim"} & : & \isaratt \\
- @{attribute_def (Pure) "dest"} & : & \isaratt \\
- @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
- @{attribute_def "OF"} & : & \isaratt \\
- @{attribute_def "of"} & : & \isaratt \\
- @{attribute_def "where"} & : & \isaratt \\
+ @{method_def "-"} & : & @{text method} \\
+ @{method_def "fact"} & : & @{text method} \\
+ @{method_def "assumption"} & : & @{text method} \\
+ @{method_def "this"} & : & @{text method} \\
+ @{method_def "rule"} & : & @{text method} \\
+ @{method_def "iprover"} & : & @{text method} \\[0.5ex]
+ @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
+ @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
+ @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
+ @{attribute_def "rule"} & : & @{text attribute} \\[0.5ex]
+ @{attribute_def "OF"} & : & @{text attribute} \\
+ @{attribute_def "of"} & : & @{text attribute} \\
+ @{attribute_def "where"} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -824,12 +824,12 @@
be used in scripts, too.
\begin{matharray}{rcl}
- @{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} \\
+ @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+ @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
\end{matharray}
\begin{rail}
@@ -891,7 +891,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
+ @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -935,8 +935,8 @@
text {*
\begin{matharray}{rcl}
- @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
- @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
+ @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
+ @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
\end{matharray}
Generalized elimination means that additional elements with certain
@@ -1015,14 +1015,14 @@
text {*
\begin{matharray}{rcl}
- @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
- @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
- @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{attribute trans} & : & \isaratt \\
- @{attribute sym} & : & \isaratt \\
- @{attribute symmetric} & : & \isaratt \\
+ @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
+ @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
+ @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute trans} & : & @{text attribute} \\
+ @{attribute sym} & : & @{text attribute} \\
+ @{attribute symmetric} & : & @{text attribute} \\
\end{matharray}
Calculational proof is forward reasoning with implicit application
@@ -1129,12 +1129,12 @@
text {*
\begin{matharray}{rcl}
- @{command_def "case"} & : & \isartrans{proof(state)}{proof(state)} \\
- @{command_def "print_cases"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
- @{attribute_def case_names} & : & \isaratt \\
- @{attribute_def case_conclusion} & : & \isaratt \\
- @{attribute_def params} & : & \isaratt \\
- @{attribute_def consumes} & : & \isaratt \\
+ @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def case_names} & : & @{text attribute} \\
+ @{attribute_def case_conclusion} & : & @{text attribute} \\
+ @{attribute_def params} & : & @{text attribute} \\
+ @{attribute_def consumes} & : & @{text attribute} \\
\end{matharray}
The puristic way to build up Isar proof contexts is by explicit
@@ -1255,9 +1255,9 @@
text {*
\begin{matharray}{rcl}
- @{method_def cases} & : & \isarmeth \\
- @{method_def induct} & : & \isarmeth \\
- @{method_def coinduct} & : & \isarmeth \\
+ @{method_def cases} & : & @{text method} \\
+ @{method_def induct} & : & @{text method} \\
+ @{method_def coinduct} & : & @{text method} \\
\end{matharray}
The @{method cases}, @{method induct}, and @{method coinduct}
@@ -1440,10 +1440,10 @@
text {*
\begin{matharray}{rcl}
- @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{attribute_def cases} & : & \isaratt \\
- @{attribute_def induct} & : & \isaratt \\
- @{attribute_def coinduct} & : & \isaratt \\
+ @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def cases} & : & @{text attribute} \\
+ @{attribute_def induct} & : & @{text attribute} \\
+ @{attribute_def coinduct} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:45:40 2008 +0100
@@ -10,8 +10,8 @@
text {*
\begin{matharray}{rcl}
- @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
- @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\
+ @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
+ @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
\end{matharray}
Isabelle/Isar theories are defined via theory files, which may
@@ -82,8 +82,8 @@
global theory context.
\begin{matharray}{rcll}
- @{command_def "context"} & : & \isartrans{theory}{local{\dsh}theory} \\
- @{command_def (local) "end"} & : & \isartrans{local{\dsh}theory}{theory} \\
+ @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
\end{matharray}
\indexouternonterm{target}
@@ -143,13 +143,13 @@
text {*
\begin{matharray}{rcll}
- @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\
- @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\
- @{attribute_def "defn"} & : & \isaratt \\
- @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "no_notation"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
+ @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{attribute_def "defn"} & : & @{text attribute} \\
+ @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
+ @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
These specification mechanisms provide a slightly more abstract view
@@ -253,8 +253,8 @@
means of an attribute.
\begin{matharray}{rcl}
- @{command_def "declaration"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "declare"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{rail}
@@ -295,11 +295,11 @@
text {*
\begin{matharray}{rcl}
- @{command_def "locale"} & : & \isartrans{theory}{local{\dsh}theory} \\
- @{command_def "print_locale"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{command_def "print_locales"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{method_def intro_locales} & : & \isarmeth \\
- @{method_def unfold_locales} & : & \isarmeth \\
+ @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{method_def intro_locales} & : & @{text method} \\
+ @{method_def unfold_locales} & : & @{text method} \\
\end{matharray}
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
@@ -461,9 +461,9 @@
"interpret"}).
\begin{matharray}{rcl}
- @{command_def "interpretation"} & : & \isartrans{theory}{proof(prove)} \\
- @{command_def "interpret"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
- @{command_def "print_interps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
+ @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
\indexouternonterm{interp}
@@ -601,12 +601,12 @@
tutorial.
\begin{matharray}{rcl}
- @{command_def "class"} & : & \isartrans{theory}{local{\dsh}theory} \\
- @{command_def "instantiation"} & : & \isartrans{theory}{local{\dsh}theory} \\
- @{command_def "instance"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
- @{command_def "subclass"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
- @{command_def "print_classes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{method_def intro_classes} & : & \isarmeth \\
+ @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{method_def intro_classes} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -716,8 +716,8 @@
text {*
\begin{matharray}{rcl}
- @{command_def "axclass"} & : & \isartrans{theory}{theory} \\
- @{command_def "instance"} & : & \isartrans{theory}{proof(prove)} \\
+ @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
\end{matharray}
Axiomatic type classes are Isabelle/Pure's primitive
@@ -772,7 +772,7 @@
end-users.
\begin{matharray}{rcl}
- @{command_def "overloading"} & : & \isartrans{theory}{local{\dsh}theory} \\
+ @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{rail}
@@ -805,12 +805,12 @@
text {*
\begin{matharray}{rcl}
- @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- @{command_def "ML_prf"} & : & \isarkeep{proof} \\
- @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
- @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
- @{command_def "setup"} & : & \isartrans{theory}{theory} \\
+ @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{mldecls}
@@ -879,10 +879,10 @@
text {*
\begin{matharray}{rcll}
- @{command_def "classes"} & : & \isartrans{theory}{theory} \\
- @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
- @{command_def "class_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
+ @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
\begin{rail}
@@ -922,10 +922,10 @@
text {*
\begin{matharray}{rcll}
- @{command_def "types"} & : & \isartrans{theory}{theory} \\
- @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
- @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
- @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
\begin{rail}
@@ -1011,9 +1011,9 @@
instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
\begin{matharray}{rcl}
- @{command_def "consts"} & : & \isartrans{theory}{theory} \\
- @{command_def "defs"} & : & \isartrans{theory}{theory} \\
- @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
+ @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -1082,9 +1082,9 @@
text {*
\begin{matharray}{rcll}
- @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
- @{command_def "theorems"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
+ @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{rail}
@@ -1135,7 +1135,7 @@
presumed theorems depend on unproven suppositions.
\begin{matharray}{rcl}
- @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
+ @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -1164,9 +1164,9 @@
text {*
\begin{matharray}{rcl}
- @{command_def "global"} & : & \isartrans{theory}{theory} \\
- @{command_def "local"} & : & \isartrans{theory}{theory} \\
- @{command_def "hide"} & : & \isartrans{theory}{theory} \\
+ @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -1211,10 +1211,10 @@
text {*
\begin{matharray}{rcl}
- @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
- @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
- @{command_def "translations"} & : & \isartrans{theory}{theory} \\
- @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
+ @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -1262,11 +1262,11 @@
text {*
\begin{matharray}{rcl}
- @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
- @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
+ @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Thu Nov 13 21:45:40 2008 +0100
@@ -16,9 +16,9 @@
Simplifier setup.
\begin{matharray}{rcl}
- @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{method_def (ZF) typecheck} & : & \isarmeth \\
- @{attribute_def (ZF) TC} & : & \isaratt \\
+ @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{method_def (ZF) typecheck} & : & @{text method} \\
+ @{attribute_def (ZF) TC} & : & @{text attribute} \\
\end{matharray}
\begin{rail}
@@ -51,10 +51,10 @@
Coinductive definitions are available in both cases, too.
\begin{matharray}{rcl}
- @{command_def (ZF) "inductive"} & : & \isartrans{theory}{theory} \\
- @{command_def (ZF) "coinductive"} & : & \isartrans{theory}{theory} \\
- @{command_def (ZF) "datatype"} & : & \isartrans{theory}{theory} \\
- @{command_def (ZF) "codatatype"} & : & \isartrans{theory}{theory} \\
+ @{command_def (ZF) "inductive"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (ZF) "coinductive"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (ZF) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -104,7 +104,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\
+ @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
@@ -121,10 +121,10 @@
ported to Isar. These should not be used in proper proof texts.
\begin{matharray}{rcl}
- @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
- @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
- @{command_def (ZF) "inductive_cases"} & : & \isartrans{theory}{theory} \\
+ @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
+ @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
--- a/doc-src/isar.sty Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/isar.sty Thu Nov 13 21:45:40 2008 +0100
@@ -20,9 +20,3 @@
\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
\newcommand{\isasymIN}{\isakeyword{in}}
\newcommand{\isasymSTRUCTURE}{\isakeyword{structure}}
-
-\newcommand{\isartrans}[2]{#1 \mathbin{\,\to\,} #2}
-\newcommand{\isarkeep}[1]{#1 \mathbin{\,\to\,} #1}
-\newcommand{\isarantiq}{antiquotation}
-\newcommand{\isarmeth}{method}
-\newcommand{\isaratt}{attribute}