# HG changeset patch # User wenzelm # Date 1226609140 -3600 # Node ID 9ec4482c9201225d57bc85e9eee6980767d95a36 # Parent cbc435f7b16b5c7b19fd12c245141c2a384b2b04 updated/refined types of Isar language elements, removed special LaTeX macros; diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/Document_Preparation.thy --- 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 \ toplevel"} \\[0.5ex] + @{command_def "chapter"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "section"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "subsection"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "subsubsection"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "text"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "text_raw"} & : & @{text "local_theory \ local_theory"} \\[0.5ex] + @{command_def "sect"} & : & @{text "proof \ proof"} \\ + @{command_def "subsect"} & : & @{text "proof \ proof"} \\ + @{command_def "subsubsect"} & : & @{text "proof \ proof"} \\ + @{command_def "txt"} & : & @{text "proof \ proof"} \\ + @{command_def "txt_raw"} & : & @{text "proof \ 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 \"} \\ + @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \"} \\ \end{matharray} \begin{rail} diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/Generic.thy --- 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 \"} \\ \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 \ a\<^sub>n"} and @{attribute folded}~@{text "a\<^sub>1 \ 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 \"} \\ + @{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 \ 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 \"} \\ + @{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 \ 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 diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/HOLCF_Specific.thy --- 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 \ theory"} \\ \end{matharray} HOLCF provides a separate type for continuous functions @{text "\ \ @@ -33,7 +33,7 @@ text {* \begin{matharray}{rcl} - @{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOLCF) "domain"} & : & @{text "theory \ theory"} \\ \end{matharray} \begin{rail} 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 \ theory"} \\ + @{command_def (HOL) "typedef"} & : & @{text "theory \ 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 \ 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 \ theory"} \\ + @{command_def (HOL) "rep_datatype"} & : & @{text "theory \ 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 \ local_theory"} \\ + @{command_def (HOL) "fun"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def (HOL) "function"} & : & @{text "local_theory \ proof(prove)"} \\ + @{command_def (HOL) "termination"} & : & @{text "local_theory \ 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 \ theory)"} \\ + @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \ 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 \ local_theory"} \\ + @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def (HOL) "coinductive"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \ 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 \"} \\ + @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + @{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 \ 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 \"} \\ + @{command_def (HOL) "code_module"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_library"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "consts_code"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "types_code"} & : & @{text "theory \ 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 \"} \\ + @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "code_datatype"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{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 \ proof(prove)"} \\ + @{command_def (HOL) "ax_specification"} & : & @{text "theory \ proof(prove)"} \\ \end{matharray} \begin{rail} diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/Misc.thy --- 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 \"} \\ + @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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 \"} \\ + @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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 \ any"} \\ + @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \ any"} \\ + @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \ 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 \"} \\ + @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \"} \\ \end{matharray} \begin{rail} diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/Proof.thy --- 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) \ proof(state)"} \\ + @{command_def "{"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "}"} & : & @{text "proof(state) \ 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 \ 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) \ proof(state)"} \\ + @{command_def "assume"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "presume"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "def"} & : & @{text "proof(state) \ 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) \ 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) \ proof(state)"} \\ + @{command_def "then"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "from"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "with"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "using"} & : & @{text "proof(prove) \ proof(prove)"} \\ + @{command_def "unfolding"} & : & @{text "proof(prove) \ 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 \ proof(prove)"} \\ + @{command_def "theorem"} & : & @{text "local_theory \ proof(prove)"} \\ + @{command_def "corollary"} & : & @{text "local_theory \ proof(prove)"} \\ + @{command_def "have"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ + @{command_def "show"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ + @{command_def "hence"} & : & @{text "proof(state) \ proof(prove)"} \\ + @{command_def "thus"} & : & @{text "proof(state) \ proof(prove)"} \\ + @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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) \ proof(state)"} \\ + @{command_def "qed"} & : & @{text "proof(state) \ proof(state) | local_theory | theory"} \\ + @{command_def "by"} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ + @{command_def ".."} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ + @{command_def "."} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ + @{command_def "sorry"} & : & @{text "proof(prove) \ 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) \ proof(prove)"} \\ + @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ + @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ + @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ + @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \ 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 \ 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) \ proof(prove)"} \\ + @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \ 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) \ proof(state)"} \\ + @{command_def "finally"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "moreover"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "ultimately"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{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) \ proof(state)"} \\ + @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{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 \"} \\ + @{attribute_def cases} & : & @{text attribute} \\ + @{attribute_def induct} & : & @{text attribute} \\ + @{attribute_def coinduct} & : & @{text attribute} \\ \end{matharray} \begin{rail} diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/Spec.thy --- 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 \ theory"} \\ + @{command_def (global) "end"} & : & @{text "theory \ 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 \ local_theory"} \\ + @{command_def (local) "end"} & : & @{text "local_theory \ 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 \ theory"} & (axiomatic!)\\ + @{command_def "definition"} & : & @{text "local_theory \ local_theory"} \\ + @{attribute_def "defn"} & : & @{text attribute} \\ + @{command_def "abbreviation"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ + @{command_def "notation"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "no_notation"} & : & @{text "local_theory \ 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 \ local_theory"} \\ + @{command_def "declare"} & : & @{text "local_theory \ 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 \ local_theory"} \\ + @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{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 \ proof(prove)"} \\ + @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \ proof(prove)"} \\ + @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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 \ local_theory"} \\ + @{command_def "instantiation"} & : & @{text "theory \ local_theory"} \\ + @{command_def "instance"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "subclass"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{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 \ theory"} \\ + @{command_def "instance"} & : & @{text "theory \ 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 \ 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 \ local_theory"} \\ + @{command_def "ML"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "ML_prf"} & : & @{text "proof \ proof"} \\ + @{command_def "ML_val"} & : & @{text "any \"} \\ + @{command_def "ML_command"} & : & @{text "any \"} \\ + @{command_def "setup"} & : & @{text "theory \ 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 \ theory"} \\ + @{command_def "classrel"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + @{command_def "defaultsort"} & : & @{text "theory \ theory"} \\ + @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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 \ theory"} \\ + @{command_def "typedecl"} & : & @{text "theory \ theory"} \\ + @{command_def "nonterminals"} & : & @{text "theory \ theory"} \\ + @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} \begin{rail} @@ -1011,9 +1011,9 @@ instance of this, general @{text "d :: \ \ \"} 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 \ theory"} \\ + @{command_def "defs"} & : & @{text "theory \ theory"} \\ + @{command_def "constdefs"} & : & @{text "theory \ 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 \ theory"} & (axiomatic!) \\ + @{command_def "lemmas"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "theorems"} & : & @{text "local_theory \ 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 \ 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 \ theory"} \\ + @{command_def "local"} & : & @{text "theory \ theory"} \\ + @{command_def "hide"} & : & @{text "theory \ 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 \ theory"} \\ + @{command_def "no_syntax"} & : & @{text "theory \ theory"} \\ + @{command_def "translations"} & : & @{text "theory \ theory"} \\ + @{command_def "no_translations"} & : & @{text "theory \ 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 \ theory"} \\ + @{command_def "parse_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "print_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "typed_print_translation"} & : & @{text "theory \ theory"} \\ + @{command_def "print_ast_translation"} & : & @{text "theory \ theory"} \\ \end{matharray} \begin{rail} diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/IsarRef/Thy/ZF_Specific.thy --- 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 \"} \\ + @{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 \ theory"} \\ + @{command_def (ZF) "coinductive"} & : & @{text "theory \ theory"} \\ + @{command_def (ZF) "datatype"} & : & @{text "theory \ theory"} \\ + @{command_def (ZF) "codatatype"} & : & @{text "theory \ 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 \ 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 \ theory"} \\ \end{matharray} \begin{rail} diff -r cbc435f7b16b -r 9ec4482c9201 doc-src/isar.sty --- 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}