merged
authorwenzelm
Thu Mar 14 21:17:40 2019 +0100 (2 months ago)
changeset 6991472301e1457b9
parent 69911 036037573080
parent 69913 ca515cf61651
child 69915 57a41389d0e2
merged
NEWS
     1.1 --- a/NEWS	Thu Mar 14 19:06:40 2019 +0100
     1.2 +++ b/NEWS	Thu Mar 14 21:17:40 2019 +0100
     1.3 @@ -40,6 +40,10 @@
     1.4  need to provide a closed expression -- without trailing semicolon. Minor
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Command keywords of kind thy_decl / thy_goal may be more specifically
     1.8 +fit into the traditional document model of "definition-statement-proof"
     1.9 +via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
    1.10 +
    1.11  
    1.12  *** Isabelle/jEdit Prover IDE ***
    1.13  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Mar 14 19:06:40 2019 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Mar 14 21:17:40 2019 +0100
     2.3 @@ -93,8 +93,8 @@
     2.4    proof documents work properly. Command keywords need to be classified
     2.5    according to their structural role in the formal text. Examples may be seen
     2.6    in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close>
     2.7 -  \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for
     2.8 -  theory-level declarations with and without proof, respectively. Additional
     2.9 +  \<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_defn\<close> for
    2.10 +  theory-level definitions with and without proof, respectively. Additional
    2.11    @{syntax tags} provide defaults for document preparation
    2.12    (\secref{sec:tags}).
    2.13  
     3.1 --- a/src/HOL/BNF_Composition.thy	Thu Mar 14 19:06:40 2019 +0100
     3.2 +++ b/src/HOL/BNF_Composition.thy	Thu Mar 14 21:17:40 2019 +0100
     3.3 @@ -11,8 +11,8 @@
     3.4  theory BNF_Composition
     3.5  imports BNF_Def
     3.6  keywords
     3.7 -  "copy_bnf" :: thy_decl and
     3.8 -  "lift_bnf" :: thy_goal
     3.9 +  "copy_bnf" :: thy_defn and
    3.10 +  "lift_bnf" :: thy_goal_defn
    3.11  begin
    3.12  
    3.13  lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"
     4.1 --- a/src/HOL/BNF_Def.thy	Thu Mar 14 19:06:40 2019 +0100
     4.2 +++ b/src/HOL/BNF_Def.thy	Thu Mar 14 21:17:40 2019 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  imports BNF_Cardinal_Arithmetic Fun_Def_Base
     4.5  keywords
     4.6    "print_bnfs" :: diag and
     4.7 -  "bnf" :: thy_goal
     4.8 +  "bnf" :: thy_goal_defn
     4.9  begin
    4.10  
    4.11  lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
     5.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Mar 14 19:06:40 2019 +0100
     5.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Mar 14 21:17:40 2019 +0100
     5.3 @@ -12,9 +12,9 @@
     5.4  theory BNF_Greatest_Fixpoint
     5.5  imports BNF_Fixpoint_Base String
     5.6  keywords
     5.7 -  "codatatype" :: thy_decl and
     5.8 -  "primcorecursive" :: thy_goal and
     5.9 -  "primcorec" :: thy_decl
    5.10 +  "codatatype" :: thy_defn and
    5.11 +  "primcorecursive" :: thy_goal_defn and
    5.12 +  "primcorec" :: thy_defn
    5.13  begin
    5.14  
    5.15  alias proj = Equiv_Relations.proj
     6.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Mar 14 19:06:40 2019 +0100
     6.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Mar 14 21:17:40 2019 +0100
     6.3 @@ -12,8 +12,8 @@
     6.4  theory BNF_Least_Fixpoint
     6.5  imports BNF_Fixpoint_Base
     6.6  keywords
     6.7 -  "datatype" :: thy_decl and
     6.8 -  "datatype_compat" :: thy_decl
     6.9 +  "datatype" :: thy_defn and
    6.10 +  "datatype_compat" :: thy_defn
    6.11  begin
    6.12  
    6.13  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
     7.1 --- a/src/HOL/Fun.thy	Thu Mar 14 19:06:40 2019 +0100
     7.2 +++ b/src/HOL/Fun.thy	Thu Mar 14 21:17:40 2019 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  
     7.5  theory Fun
     7.6    imports Set
     7.7 -  keywords "functor" :: thy_goal
     7.8 +  keywords "functor" :: thy_goal_defn
     7.9  begin
    7.10  
    7.11  lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
     8.1 --- a/src/HOL/Fun_Def.thy	Thu Mar 14 19:06:40 2019 +0100
     8.2 +++ b/src/HOL/Fun_Def.thy	Thu Mar 14 21:17:40 2019 +0100
     8.3 @@ -7,8 +7,8 @@
     8.4  theory Fun_Def
     8.5    imports Basic_BNF_LFPs Partial_Function SAT
     8.6    keywords
     8.7 -    "function" "termination" :: thy_goal and
     8.8 -    "fun" "fun_cases" :: thy_decl
     8.9 +    "function" "termination" :: thy_goal_defn and
    8.10 +    "fun" "fun_cases" :: thy_defn
    8.11  begin
    8.12  
    8.13  subsection \<open>Definitions with default value\<close>
     9.1 --- a/src/HOL/HOLCF/Cpodef.thy	Thu Mar 14 19:06:40 2019 +0100
     9.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Thu Mar 14 21:17:40 2019 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  
     9.5  theory Cpodef
     9.6    imports Adm
     9.7 -  keywords "pcpodef" "cpodef" :: thy_goal
     9.8 +  keywords "pcpodef" "cpodef" :: thy_goal_defn
     9.9  begin
    9.10  
    9.11  subsection \<open>Proving a subtype is a partial order\<close>
    10.1 --- a/src/HOL/HOLCF/Domain.thy	Thu Mar 14 19:06:40 2019 +0100
    10.2 +++ b/src/HOL/HOLCF/Domain.thy	Thu Mar 14 21:17:40 2019 +0100
    10.3 @@ -8,7 +8,8 @@
    10.4  imports Representable Domain_Aux
    10.5  keywords
    10.6    "lazy" "unsafe" and
    10.7 -  "domaindef" "domain_isomorphism" "domain" :: thy_decl
    10.8 +  "domaindef" "domain" :: thy_defn and
    10.9 +  "domain_isomorphism" :: thy_decl
   10.10  begin
   10.11  
   10.12  default_sort "domain"
    11.1 --- a/src/HOL/HOLCF/Fixrec.thy	Thu Mar 14 19:06:40 2019 +0100
    11.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Thu Mar 14 21:17:40 2019 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  
    11.5  theory Fixrec
    11.6  imports Cprod Sprod Ssum Up One Tr Fix
    11.7 -keywords "fixrec" :: thy_decl
    11.8 +keywords "fixrec" :: thy_defn
    11.9  begin
   11.10  
   11.11  subsection \<open>Pattern-match monad\<close>
    12.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Mar 14 19:06:40 2019 +0100
    12.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 14 21:17:40 2019 +0100
    12.3 @@ -8,7 +8,7 @@
    12.4  
    12.5  theory Hilbert_Choice
    12.6    imports Wellfounded
    12.7 -  keywords "specification" :: thy_goal
    12.8 +  keywords "specification" :: thy_goal_defn
    12.9  begin
   12.10  
   12.11  subsection \<open>Hilbert's epsilon\<close>
    13.1 --- a/src/HOL/Inductive.thy	Thu Mar 14 19:06:40 2019 +0100
    13.2 +++ b/src/HOL/Inductive.thy	Thu Mar 14 21:17:40 2019 +0100
    13.3 @@ -7,11 +7,11 @@
    13.4  theory Inductive
    13.5    imports Complete_Lattices Ctr_Sugar
    13.6    keywords
    13.7 -    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
    13.8 +    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_defn and
    13.9      "monos" and
   13.10      "print_inductives" :: diag and
   13.11      "old_rep_datatype" :: thy_goal and
   13.12 -    "primrec" :: thy_decl
   13.13 +    "primrec" :: thy_defn
   13.14  begin
   13.15  
   13.16  subsection \<open>Least fixed points\<close>
    14.1 --- a/src/HOL/Library/BNF_Corec.thy	Thu Mar 14 19:06:40 2019 +0100
    14.2 +++ b/src/HOL/Library/BNF_Corec.thy	Thu Mar 14 21:17:40 2019 +0100
    14.3 @@ -12,9 +12,9 @@
    14.4  theory BNF_Corec
    14.5  imports Main
    14.6  keywords
    14.7 -  "corec" :: thy_decl and
    14.8 -  "corecursive" :: thy_goal and
    14.9 -  "friend_of_corec" :: thy_goal and
   14.10 +  "corec" :: thy_defn and
   14.11 +  "corecursive" :: thy_goal_defn and
   14.12 +  "friend_of_corec" :: thy_goal_defn and
   14.13    "coinduction_upto" :: thy_decl
   14.14  begin
   14.15  
    15.1 --- a/src/HOL/Library/Datatype_Records.thy	Thu Mar 14 19:06:40 2019 +0100
    15.2 +++ b/src/HOL/Library/Datatype_Records.thy	Thu Mar 14 21:17:40 2019 +0100
    15.3 @@ -6,7 +6,7 @@
    15.4  
    15.5  theory Datatype_Records
    15.6  imports Main
    15.7 -keywords "datatype_record" :: thy_decl
    15.8 +keywords "datatype_record" :: thy_defn
    15.9  begin
   15.10  
   15.11  text \<open>
    16.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 14 19:06:40 2019 +0100
    16.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 14 21:17:40 2019 +0100
    16.3 @@ -7,7 +7,7 @@
    16.4  theory Old_Recdef
    16.5  imports Main
    16.6  keywords
    16.7 -  "recdef" :: thy_decl and
    16.8 +  "recdef" :: thy_defn and
    16.9    "permissive" "congs" "hints"
   16.10  begin
   16.11  
    17.1 --- a/src/HOL/Lifting.thy	Thu Mar 14 19:06:40 2019 +0100
    17.2 +++ b/src/HOL/Lifting.thy	Thu Mar 14 21:17:40 2019 +0100
    17.3 @@ -10,7 +10,7 @@
    17.4  keywords
    17.5    "parametric" and
    17.6    "print_quot_maps" "print_quotients" :: diag and
    17.7 -  "lift_definition" :: thy_goal and
    17.8 +  "lift_definition" :: thy_goal_defn and
    17.9    "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
   17.10  begin
   17.11  
    18.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Mar 14 19:06:40 2019 +0100
    18.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 14 21:17:40 2019 +0100
    18.3 @@ -1,8 +1,10 @@
    18.4  theory Nominal 
    18.5  imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
    18.6  keywords
    18.7 -  "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
    18.8 -  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
    18.9 +  "atom_decl" :: thy_decl and
   18.10 +  "nominal_datatype" :: thy_defn and
   18.11 +  "equivariance" :: thy_decl and
   18.12 +  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal_defn and
   18.13    "avoids"
   18.14  begin
   18.15  
    19.1 --- a/src/HOL/Partial_Function.thy	Thu Mar 14 19:06:40 2019 +0100
    19.2 +++ b/src/HOL/Partial_Function.thy	Thu Mar 14 21:17:40 2019 +0100
    19.3 @@ -6,7 +6,7 @@
    19.4  
    19.5  theory Partial_Function
    19.6    imports Complete_Partial_Order Option
    19.7 -  keywords "partial_function" :: thy_decl
    19.8 +  keywords "partial_function" :: thy_defn
    19.9  begin
   19.10  
   19.11  named_theorems partial_function_mono "monotonicity rules for partial function definitions"
    20.1 --- a/src/HOL/Product_Type.thy	Thu Mar 14 19:06:40 2019 +0100
    20.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 14 21:17:40 2019 +0100
    20.3 @@ -7,7 +7,7 @@
    20.4  
    20.5  theory Product_Type
    20.6    imports Typedef Inductive Fun
    20.7 -  keywords "inductive_set" "coinductive_set" :: thy_decl
    20.8 +  keywords "inductive_set" "coinductive_set" :: thy_defn
    20.9  begin
   20.10  
   20.11  subsection \<open>\<^typ>\<open>bool\<close> is a datatype\<close>
    21.1 --- a/src/HOL/Quotient.thy	Thu Mar 14 19:06:40 2019 +0100
    21.2 +++ b/src/HOL/Quotient.thy	Thu Mar 14 21:17:40 2019 +0100
    21.3 @@ -8,8 +8,8 @@
    21.4  imports Lifting
    21.5  keywords
    21.6    "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
    21.7 -  "quotient_type" :: thy_goal and "/" and
    21.8 -  "quotient_definition" :: thy_goal
    21.9 +  "quotient_type" :: thy_goal_defn and "/" and
   21.10 +  "quotient_definition" :: thy_goal_defn
   21.11  begin
   21.12  
   21.13  text \<open>
    22.1 --- a/src/HOL/Record.thy	Thu Mar 14 19:06:40 2019 +0100
    22.2 +++ b/src/HOL/Record.thy	Thu Mar 14 21:17:40 2019 +0100
    22.3 @@ -11,7 +11,7 @@
    22.4  theory Record
    22.5  imports Quickcheck_Exhaustive
    22.6  keywords
    22.7 -  "record" :: thy_decl and
    22.8 +  "record" :: thy_defn and
    22.9    "print_record" :: diag
   22.10  begin
   22.11  
    23.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 14 19:06:40 2019 +0100
    23.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 14 21:17:40 2019 +0100
    23.3 @@ -5,7 +5,7 @@
    23.4  section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close>
    23.5  
    23.6  theory StateSpaceLocale imports StateFun 
    23.7 -keywords "statespace" :: thy_decl
    23.8 +keywords "statespace" :: thy_defn
    23.9  begin
   23.10  
   23.11  ML_file \<open>state_space.ML\<close>
    24.1 --- a/src/HOL/Typedef.thy	Thu Mar 14 19:06:40 2019 +0100
    24.2 +++ b/src/HOL/Typedef.thy	Thu Mar 14 21:17:40 2019 +0100
    24.3 @@ -7,7 +7,7 @@
    24.4  theory Typedef
    24.5  imports Set
    24.6  keywords
    24.7 -  "typedef" :: thy_goal and
    24.8 +  "typedef" :: thy_goal_defn and
    24.9    "morphisms" :: quasi_command
   24.10  begin
   24.11  
    25.1 --- a/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Thu Mar 14 19:06:40 2019 +0100
    25.2 +++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Thu Mar 14 21:17:40 2019 +0100
    25.3 @@ -4,7 +4,7 @@
    25.4  
    25.5  theory Prerequisites
    25.6    imports Main
    25.7 -  keywords "lemmas_with"::thy_decl
    25.8 +  keywords "lemmas_with" :: thy_decl
    25.9  begin
   25.10  
   25.11  context
    26.1 --- a/src/Pure/Isar/keyword.ML	Thu Mar 14 19:06:40 2019 +0100
    26.2 +++ b/src/Pure/Isar/keyword.ML	Thu Mar 14 21:17:40 2019 +0100
    26.3 @@ -14,8 +14,12 @@
    26.4    val thy_end: string
    26.5    val thy_decl: string
    26.6    val thy_decl_block: string
    26.7 +  val thy_defn: string
    26.8 +  val thy_stmt: string
    26.9    val thy_load: string
   26.10    val thy_goal: string
   26.11 +  val thy_goal_defn: string
   26.12 +  val thy_goal_stmt: string
   26.13    val qed: string
   26.14    val qed_script: string
   26.15    val qed_block: string
   26.16 @@ -93,8 +97,12 @@
   26.17  val thy_end = "thy_end";
   26.18  val thy_decl = "thy_decl";
   26.19  val thy_decl_block = "thy_decl_block";
   26.20 +val thy_defn = "thy_defn";
   26.21 +val thy_stmt = "thy_stmt";
   26.22  val thy_load = "thy_load";
   26.23  val thy_goal = "thy_goal";
   26.24 +val thy_goal_defn = "thy_goal_defn";
   26.25 +val thy_goal_stmt = "thy_goal_stmt";
   26.26  val qed = "qed";
   26.27  val qed_script = "qed_script";
   26.28  val qed_block = "qed_block";
   26.29 @@ -117,9 +125,9 @@
   26.30  
   26.31  val command_kinds =
   26.32    [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
   26.33 -    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block,
   26.34 -    next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script,
   26.35 -    prf_script_goal, prf_script_asm_goal];
   26.36 +    thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script,
   26.37 +    qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain,
   26.38 +    prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal];
   26.39  
   26.40  
   26.41  (* specifications *)
   26.42 @@ -256,10 +264,11 @@
   26.43  val is_theory_load = command_category [thy_load];
   26.44  
   26.45  val is_theory = command_category
   26.46 -  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
   26.47 +  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal,
   26.48 +    thy_goal_defn, thy_goal_stmt];
   26.49  
   26.50  val is_theory_body = command_category
   26.51 -  [thy_load, thy_decl, thy_decl_block, thy_goal];
   26.52 +  [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt];
   26.53  
   26.54  val is_proof = command_category
   26.55    [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open,
   26.56 @@ -271,7 +280,7 @@
   26.57      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
   26.58      prf_script_asm_goal];
   26.59  
   26.60 -val is_theory_goal = command_category [thy_goal];
   26.61 +val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt];
   26.62  val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
   26.63  val is_qed = command_category [qed, qed_script, qed_block];
   26.64  val is_qed_global = command_category [qed_global];
    27.1 --- a/src/Pure/Isar/keyword.scala	Thu Mar 14 19:06:40 2019 +0100
    27.2 +++ b/src/Pure/Isar/keyword.scala	Thu Mar 14 21:17:40 2019 +0100
    27.3 @@ -21,8 +21,12 @@
    27.4    val THY_END = "thy_end"
    27.5    val THY_DECL = "thy_decl"
    27.6    val THY_DECL_BLOCK = "thy_decl_block"
    27.7 +  val THY_DEFN = "thy_defn"
    27.8 +  val THY_STMT = "thy_stmt"
    27.9    val THY_LOAD = "thy_load"
   27.10    val THY_GOAL = "thy_goal"
   27.11 +  val THY_GOAL_DEFN = "thy_goal_defn"
   27.12 +  val THY_GOAL_STMT = "thy_goal_stmt"
   27.13    val QED = "qed"
   27.14    val QED_SCRIPT = "qed_script"
   27.15    val QED_BLOCK = "qed_block"
   27.16 @@ -60,11 +64,15 @@
   27.17  
   27.18    val theory_load = Set(THY_LOAD)
   27.19  
   27.20 -  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
   27.21 +  val theory =
   27.22 +    Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
   27.23 +      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
   27.24  
   27.25    val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
   27.26  
   27.27 -  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
   27.28 +  val theory_body =
   27.29 +    Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
   27.30 +      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
   27.31  
   27.32    val prf_script = Set(PRF_SCRIPT)
   27.33  
   27.34 @@ -78,7 +86,7 @@
   27.35        PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
   27.36        PRF_SCRIPT_ASM_GOAL)
   27.37  
   27.38 -  val theory_goal = Set(THY_GOAL)
   27.39 +  val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
   27.40    val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
   27.41    val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   27.42    val qed_global = Set(QED_GLOBAL)
    28.1 --- a/src/Pure/Pure.thy	Thu Mar 14 19:06:40 2019 +0100
    28.2 +++ b/src/Pure/Pure.thy	Thu Mar 14 21:17:40 2019 +0100
    28.3 @@ -15,11 +15,11 @@
    28.4    and "text" "txt" :: document_body
    28.5    and "text_raw" :: document_raw
    28.6    and "default_sort" :: thy_decl
    28.7 -  and "typedecl" "type_synonym" "nonterminal" "judgment"
    28.8 -    "consts" "syntax" "no_syntax" "translations" "no_translations"
    28.9 -    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
   28.10 -    "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
   28.11 -    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   28.12 +  and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations"
   28.13 +    "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias"
   28.14 +    "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   28.15 +  and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn
   28.16 +  and "axiomatization" :: thy_stmt
   28.17    and "external_file" "bibtex_file" :: thy_load
   28.18    and "generate_file" :: thy_decl
   28.19    and "export_generated_files" :: diag
   28.20 @@ -46,8 +46,8 @@
   28.21    and "instance" :: thy_goal
   28.22    and "overloading" :: thy_decl_block
   28.23    and "code_datatype" :: thy_decl
   28.24 -  and "theorem" "lemma" "corollary" "proposition" :: thy_goal
   28.25 -  and "schematic_goal" :: thy_goal
   28.26 +  and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt
   28.27 +  and "schematic_goal" :: thy_goal_stmt
   28.28    and "notepad" :: thy_decl_block
   28.29    and "have" :: prf_goal % "proof"
   28.30    and "hence" :: prf_goal % "proof"