--- 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 ***
--- 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}).
--- 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"
--- 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)"
--- 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
--- 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> {}"
--- 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"
--- 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>
--- 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>
--- 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"
--- 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>
--- 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>
--- 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>
--- 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
--- 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>
--- 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
--- 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
--- 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
--- 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"
--- 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>
--- 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>
--- 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
--- 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>
--- 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
--- 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
--- 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];
--- 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)
--- 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"