--- a/etc/isar-keywords-ZF.el Fri Mar 14 15:26:52 2014 +0100
+++ b/etc/isar-keywords-ZF.el Fri Mar 14 15:41:29 2014 +0100
@@ -367,6 +367,7 @@
"hide_fact"
"hide_type"
"inductive"
+ "inductive_cases"
"instantiation"
"judgment"
"lemmas"
@@ -404,7 +405,7 @@
"typedecl"))
(defconst isar-keywords-theory-script
- '("inductive_cases"))
+ '())
(defconst isar-keywords-theory-goal
'("corollary"
--- a/etc/isar-keywords.el Fri Mar 14 15:26:52 2014 +0100
+++ b/etc/isar-keywords.el Fri Mar 14 15:41:29 2014 +0100
@@ -530,7 +530,9 @@
"import_tptp"
"import_type_map"
"inductive"
+ "inductive_cases"
"inductive_set"
+ "inductive_simps"
"instantiation"
"judgment"
"lemmas"
@@ -590,8 +592,7 @@
"typedecl"))
(defconst isar-keywords-theory-script
- '("inductive_cases"
- "inductive_simps"))
+ '())
(defconst isar-keywords-theory-goal
'("ax_specification"
--- a/src/HOL/Inductive.thy Fri Mar 14 15:26:52 2014 +0100
+++ b/src/HOL/Inductive.thy Fri Mar 14 15:41:29 2014 +0100
@@ -7,8 +7,8 @@
theory Inductive
imports Complete_Lattices Ctr_Sugar
keywords
- "inductive" "coinductive" :: thy_decl and
- "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+ "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
+ "monos" and
"print_inductives" :: diag and
"rep_datatype" :: thy_goal and
"primrec" :: thy_decl
--- a/src/Pure/Isar/keyword.ML Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Pure/Isar/keyword.ML Fri Mar 14 15:41:29 2014 +0100
@@ -20,7 +20,6 @@
val thy_decl: T
val thy_load: T
val thy_load_files: string list -> T
- val thy_script: T
val thy_goal: T
val qed: T
val qed_script: T
@@ -101,7 +100,6 @@
val thy_decl = kind "thy_decl";
val thy_load = kind "thy_load";
fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
-val thy_script = kind "thy_script";
val thy_goal = kind "thy_goal";
val qed = kind "qed";
val qed_script = kind "qed_script";
@@ -123,7 +121,7 @@
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
+ thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
@@ -249,7 +247,7 @@
val is_theory = command_category
[thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal];
+ thy_load, thy_decl, thy_goal];
val is_proof = command_category
[qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
--- a/src/Pure/Isar/keyword.scala Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Pure/Isar/keyword.scala Fri Mar 14 15:41:29 2014 +0100
@@ -22,7 +22,6 @@
val THY_HEADING4 = "thy_heading4"
val THY_DECL = "thy_decl"
val THY_LOAD = "thy_load"
- val THY_SCRIPT = "thy_script"
val THY_GOAL = "thy_goal"
val QED = "qed"
val QED_SCRIPT = "qed_script"
@@ -50,7 +49,7 @@
val diag = Set(DIAG)
val theory =
Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
- THY_DECL, THY_SCRIPT, THY_GOAL)
+ THY_DECL, THY_GOAL)
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
@@ -61,6 +60,5 @@
Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
PRF_CHAIN, PRF_DECL)
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
- val improper = Set(THY_SCRIPT, PRF_SCRIPT)
}
--- a/src/Pure/Tools/keywords.scala Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Pure/Tools/keywords.scala Fri Mar 14 15:41:29 2014 +0100
@@ -25,7 +25,6 @@
"thy_heading4" -> "theory-heading",
"thy_load" -> "theory-decl",
"thy_decl" -> "theory-decl",
- "thy_script" -> "theory-script",
"thy_goal" -> "theory-goal",
"qed_script" -> "qed",
"qed_block" -> "qed-block",
--- a/src/Tools/jEdit/src/rendering.scala Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Fri Mar 14 15:41:29 2014 +0100
@@ -53,7 +53,6 @@
import JEditToken._
Map[String, Byte](
Keyword.THY_END -> KEYWORD2,
- Keyword.THY_SCRIPT -> LABEL,
Keyword.QED_SCRIPT -> DIGIT,
Keyword.PRF_SCRIPT -> DIGIT,
Keyword.PRF_ASM -> KEYWORD3,
--- a/src/ZF/Inductive_ZF.thy Fri Mar 14 15:26:52 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy Fri Mar 14 15:41:29 2014 +0100
@@ -14,8 +14,7 @@
theory Inductive_ZF
imports Fixedpt QPair Nat_ZF
keywords
- "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
- "inductive_cases" :: thy_script and
+ "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
"domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
"elimination" "induction" "case_eqns" "recursor_eqns"
begin