# HG changeset patch
# User wenzelm
# Date 1552594660 -3600
# Node ID 72301e1457b9c48b445f03571efebab09efb6aaf
# Parent  0360375730801a9978ec279042395f1daf327b7c# Parent  ca515cf6165155a109fb11420c522a22e726e56f
merged

diff -r 036037573080 -r 72301e1457b9 NEWS
--- a/NEWS	Thu Mar 14 19:06:40 2019 +0100
+++ b/NEWS	Thu Mar 14 21:17:40 2019 +0100
@@ -40,6 +40,10 @@
 need to provide a closed expression -- without trailing semicolon. Minor
 INCOMPATIBILITY.
 
+* Command keywords of kind thy_decl / thy_goal may be more specifically
+fit into the traditional document model of "definition-statement-proof"
+via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
+
 
 *** Isabelle/jEdit Prover IDE ***
 
diff -r 036037573080 -r 72301e1457b9 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -93,8 +93,8 @@
   proof documents work properly. Command keywords need to be classified
   according to their structural role in the formal text. Examples may be seen
   in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close>
-  \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for
-  theory-level declarations with and without proof, respectively. Additional
+  \<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_defn\<close> for
+  theory-level definitions with and without proof, respectively. Additional
   @{syntax tags} provide defaults for document preparation
   (\secref{sec:tags}).
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/BNF_Composition.thy
--- a/src/HOL/BNF_Composition.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/BNF_Composition.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -11,8 +11,8 @@
 theory BNF_Composition
 imports BNF_Def
 keywords
-  "copy_bnf" :: thy_decl and
-  "lift_bnf" :: thy_goal
+  "copy_bnf" :: thy_defn and
+  "lift_bnf" :: thy_goal_defn
 begin
 
 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"
diff -r 036037573080 -r 72301e1457b9 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/BNF_Def.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -12,7 +12,7 @@
 imports BNF_Cardinal_Arithmetic Fun_Def_Base
 keywords
   "print_bnfs" :: diag and
-  "bnf" :: thy_goal
+  "bnf" :: thy_goal_defn
 begin
 
 lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
diff -r 036037573080 -r 72301e1457b9 src/HOL/BNF_Greatest_Fixpoint.thy
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -12,9 +12,9 @@
 theory BNF_Greatest_Fixpoint
 imports BNF_Fixpoint_Base String
 keywords
-  "codatatype" :: thy_decl and
-  "primcorecursive" :: thy_goal and
-  "primcorec" :: thy_decl
+  "codatatype" :: thy_defn and
+  "primcorecursive" :: thy_goal_defn and
+  "primcorec" :: thy_defn
 begin
 
 alias proj = Equiv_Relations.proj
diff -r 036037573080 -r 72301e1457b9 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -12,8 +12,8 @@
 theory BNF_Least_Fixpoint
 imports BNF_Fixpoint_Base
 keywords
-  "datatype" :: thy_decl and
-  "datatype_compat" :: thy_decl
+  "datatype" :: thy_defn and
+  "datatype_compat" :: thy_defn
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
diff -r 036037573080 -r 72301e1457b9 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Fun.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -8,7 +8,7 @@
 
 theory Fun
   imports Set
-  keywords "functor" :: thy_goal
+  keywords "functor" :: thy_goal_defn
 begin
 
 lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
diff -r 036037573080 -r 72301e1457b9 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Fun_Def.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -7,8 +7,8 @@
 theory Fun_Def
   imports Basic_BNF_LFPs Partial_Function SAT
   keywords
-    "function" "termination" :: thy_goal and
-    "fun" "fun_cases" :: thy_decl
+    "function" "termination" :: thy_goal_defn and
+    "fun" "fun_cases" :: thy_defn
 begin
 
 subsection \<open>Definitions with default value\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -6,7 +6,7 @@
 
 theory Cpodef
   imports Adm
-  keywords "pcpodef" "cpodef" :: thy_goal
+  keywords "pcpodef" "cpodef" :: thy_goal_defn
 begin
 
 subsection \<open>Proving a subtype is a partial order\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -8,7 +8,8 @@
 imports Representable Domain_Aux
 keywords
   "lazy" "unsafe" and
-  "domaindef" "domain_isomorphism" "domain" :: thy_decl
+  "domaindef" "domain" :: thy_defn and
+  "domain_isomorphism" :: thy_decl
 begin
 
 default_sort "domain"
diff -r 036037573080 -r 72301e1457b9 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -6,7 +6,7 @@
 
 theory Fixrec
 imports Cprod Sprod Ssum Up One Tr Fix
-keywords "fixrec" :: thy_decl
+keywords "fixrec" :: thy_defn
 begin
 
 subsection \<open>Pattern-match monad\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -8,7 +8,7 @@
 
 theory Hilbert_Choice
   imports Wellfounded
-  keywords "specification" :: thy_goal
+  keywords "specification" :: thy_goal_defn
 begin
 
 subsection \<open>Hilbert's epsilon\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Inductive.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -7,11 +7,11 @@
 theory Inductive
   imports Complete_Lattices Ctr_Sugar
   keywords
-    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
+    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_defn and
     "monos" and
     "print_inductives" :: diag and
     "old_rep_datatype" :: thy_goal and
-    "primrec" :: thy_decl
+    "primrec" :: thy_defn
 begin
 
 subsection \<open>Least fixed points\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Library/BNF_Corec.thy
--- a/src/HOL/Library/BNF_Corec.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Library/BNF_Corec.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -12,9 +12,9 @@
 theory BNF_Corec
 imports Main
 keywords
-  "corec" :: thy_decl and
-  "corecursive" :: thy_goal and
-  "friend_of_corec" :: thy_goal and
+  "corec" :: thy_defn and
+  "corecursive" :: thy_goal_defn and
+  "friend_of_corec" :: thy_goal_defn and
   "coinduction_upto" :: thy_decl
 begin
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Library/Datatype_Records.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -6,7 +6,7 @@
 
 theory Datatype_Records
 imports Main
-keywords "datatype_record" :: thy_decl
+keywords "datatype_record" :: thy_defn
 begin
 
 text \<open>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Library/Old_Recdef.thy
--- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -7,7 +7,7 @@
 theory Old_Recdef
 imports Main
 keywords
-  "recdef" :: thy_decl and
+  "recdef" :: thy_defn and
   "permissive" "congs" "hints"
 begin
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Lifting.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -10,7 +10,7 @@
 keywords
   "parametric" and
   "print_quot_maps" "print_quotients" :: diag and
-  "lift_definition" :: thy_goal and
+  "lift_definition" :: thy_goal_defn and
   "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
 begin
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -1,8 +1,10 @@
 theory Nominal 
 imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
 keywords
-  "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
-  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
+  "atom_decl" :: thy_decl and
+  "nominal_datatype" :: thy_defn and
+  "equivariance" :: thy_decl and
+  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal_defn and
   "avoids"
 begin
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Partial_Function.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -6,7 +6,7 @@
 
 theory Partial_Function
   imports Complete_Partial_Order Option
-  keywords "partial_function" :: thy_decl
+  keywords "partial_function" :: thy_defn
 begin
 
 named_theorems partial_function_mono "monotonicity rules for partial function definitions"
diff -r 036037573080 -r 72301e1457b9 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -7,7 +7,7 @@
 
 theory Product_Type
   imports Typedef Inductive Fun
-  keywords "inductive_set" "coinductive_set" :: thy_decl
+  keywords "inductive_set" "coinductive_set" :: thy_defn
 begin
 
 subsection \<open>\<^typ>\<open>bool\<close> is a datatype\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Quotient.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -8,8 +8,8 @@
 imports Lifting
 keywords
   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
-  "quotient_type" :: thy_goal and "/" and
-  "quotient_definition" :: thy_goal
+  "quotient_type" :: thy_goal_defn and "/" and
+  "quotient_definition" :: thy_goal_defn
 begin
 
 text \<open>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Record.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -11,7 +11,7 @@
 theory Record
 imports Quickcheck_Exhaustive
 keywords
-  "record" :: thy_decl and
+  "record" :: thy_defn and
   "print_record" :: diag
 begin
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -5,7 +5,7 @@
 section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close>
 
 theory StateSpaceLocale imports StateFun 
-keywords "statespace" :: thy_decl
+keywords "statespace" :: thy_defn
 begin
 
 ML_file \<open>state_space.ML\<close>
diff -r 036037573080 -r 72301e1457b9 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Typedef.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -7,7 +7,7 @@
 theory Typedef
 imports Set
 keywords
-  "typedef" :: thy_goal and
+  "typedef" :: thy_goal_defn and
   "morphisms" :: quasi_command
 begin
 
diff -r 036037573080 -r 72301e1457b9 src/HOL/Types_To_Sets/Examples/Prerequisites.thy
--- a/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -4,7 +4,7 @@
 
 theory Prerequisites
   imports Main
-  keywords "lemmas_with"::thy_decl
+  keywords "lemmas_with" :: thy_decl
 begin
 
 context
diff -r 036037573080 -r 72301e1457b9 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Mar 14 21:17:40 2019 +0100
@@ -14,8 +14,12 @@
   val thy_end: string
   val thy_decl: string
   val thy_decl_block: string
+  val thy_defn: string
+  val thy_stmt: string
   val thy_load: string
   val thy_goal: string
+  val thy_goal_defn: string
+  val thy_goal_stmt: string
   val qed: string
   val qed_script: string
   val qed_block: string
@@ -93,8 +97,12 @@
 val thy_end = "thy_end";
 val thy_decl = "thy_decl";
 val thy_decl_block = "thy_decl_block";
+val thy_defn = "thy_defn";
+val thy_stmt = "thy_stmt";
 val thy_load = "thy_load";
 val thy_goal = "thy_goal";
+val thy_goal_defn = "thy_goal_defn";
+val thy_goal_stmt = "thy_goal_stmt";
 val qed = "qed";
 val qed_script = "qed_script";
 val qed_block = "qed_block";
@@ -117,9 +125,9 @@
 
 val command_kinds =
   [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
-    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block,
-    next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script,
-    prf_script_goal, prf_script_asm_goal];
+    thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script,
+    qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain,
+    prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal];
 
 
 (* specifications *)
@@ -256,10 +264,11 @@
 val is_theory_load = command_category [thy_load];
 
 val is_theory = command_category
-  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
+  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal,
+    thy_goal_defn, thy_goal_stmt];
 
 val is_theory_body = command_category
-  [thy_load, thy_decl, thy_decl_block, thy_goal];
+  [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt];
 
 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open,
@@ -271,7 +280,7 @@
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
     prf_script_asm_goal];
 
-val is_theory_goal = command_category [thy_goal];
+val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
diff -r 036037573080 -r 72301e1457b9 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/Pure/Isar/keyword.scala	Thu Mar 14 21:17:40 2019 +0100
@@ -21,8 +21,12 @@
   val THY_END = "thy_end"
   val THY_DECL = "thy_decl"
   val THY_DECL_BLOCK = "thy_decl_block"
+  val THY_DEFN = "thy_defn"
+  val THY_STMT = "thy_stmt"
   val THY_LOAD = "thy_load"
   val THY_GOAL = "thy_goal"
+  val THY_GOAL_DEFN = "thy_goal_defn"
+  val THY_GOAL_STMT = "thy_goal_stmt"
   val QED = "qed"
   val QED_SCRIPT = "qed_script"
   val QED_BLOCK = "qed_block"
@@ -60,11 +64,15 @@
 
   val theory_load = Set(THY_LOAD)
 
-  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
+  val theory =
+    Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
+      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
 
   val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
 
-  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
+  val theory_body =
+    Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_DEFN, THY_STMT,
+      THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
 
   val prf_script = Set(PRF_SCRIPT)
 
@@ -78,7 +86,7 @@
       PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
       PRF_SCRIPT_ASM_GOAL)
 
-  val theory_goal = Set(THY_GOAL)
+  val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT)
   val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
   val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   val qed_global = Set(QED_GLOBAL)
diff -r 036037573080 -r 72301e1457b9 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Mar 14 19:06:40 2019 +0100
+++ b/src/Pure/Pure.thy	Thu Mar 14 21:17:40 2019 +0100
@@ -15,11 +15,11 @@
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl
-  and "typedecl" "type_synonym" "nonterminal" "judgment"
-    "consts" "syntax" "no_syntax" "translations" "no_translations"
-    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
-    "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
-    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+  and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations"
+    "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias"
+    "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+  and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn
+  and "axiomatization" :: thy_stmt
   and "external_file" "bibtex_file" :: thy_load
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
@@ -46,8 +46,8 @@
   and "instance" :: thy_goal
   and "overloading" :: thy_decl_block
   and "code_datatype" :: thy_decl
-  and "theorem" "lemma" "corollary" "proposition" :: thy_goal
-  and "schematic_goal" :: thy_goal
+  and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt
+  and "schematic_goal" :: thy_goal_stmt
   and "notepad" :: thy_decl_block
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof"