1.1 --- a/etc/isar-keywords-ZF.el Fri Mar 14 15:26:52 2014 +0100
1.2 +++ b/etc/isar-keywords-ZF.el Fri Mar 14 15:41:29 2014 +0100
1.3 @@ -367,6 +367,7 @@
1.4 "hide_fact"
1.5 "hide_type"
1.6 "inductive"
1.7 + "inductive_cases"
1.8 "instantiation"
1.9 "judgment"
1.10 "lemmas"
1.11 @@ -404,7 +405,7 @@
1.12 "typedecl"))
1.13
1.14 (defconst isar-keywords-theory-script
1.15 - '("inductive_cases"))
1.16 + '())
1.17
1.18 (defconst isar-keywords-theory-goal
1.19 '("corollary"
2.1 --- a/etc/isar-keywords.el Fri Mar 14 15:26:52 2014 +0100
2.2 +++ b/etc/isar-keywords.el Fri Mar 14 15:41:29 2014 +0100
2.3 @@ -530,7 +530,9 @@
2.4 "import_tptp"
2.5 "import_type_map"
2.6 "inductive"
2.7 + "inductive_cases"
2.8 "inductive_set"
2.9 + "inductive_simps"
2.10 "instantiation"
2.11 "judgment"
2.12 "lemmas"
2.13 @@ -590,8 +592,7 @@
2.14 "typedecl"))
2.15
2.16 (defconst isar-keywords-theory-script
2.17 - '("inductive_cases"
2.18 - "inductive_simps"))
2.19 + '())
2.20
2.21 (defconst isar-keywords-theory-goal
2.22 '("ax_specification"
3.1 --- a/src/HOL/Inductive.thy Fri Mar 14 15:26:52 2014 +0100
3.2 +++ b/src/HOL/Inductive.thy Fri Mar 14 15:41:29 2014 +0100
3.3 @@ -7,8 +7,8 @@
3.4 theory Inductive
3.5 imports Complete_Lattices Ctr_Sugar
3.6 keywords
3.7 - "inductive" "coinductive" :: thy_decl and
3.8 - "inductive_cases" "inductive_simps" :: thy_script and "monos" and
3.9 + "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
3.10 + "monos" and
3.11 "print_inductives" :: diag and
3.12 "rep_datatype" :: thy_goal and
3.13 "primrec" :: thy_decl
4.1 --- a/src/Pure/Isar/keyword.ML Fri Mar 14 15:26:52 2014 +0100
4.2 +++ b/src/Pure/Isar/keyword.ML Fri Mar 14 15:41:29 2014 +0100
4.3 @@ -20,7 +20,6 @@
4.4 val thy_decl: T
4.5 val thy_load: T
4.6 val thy_load_files: string list -> T
4.7 - val thy_script: T
4.8 val thy_goal: T
4.9 val qed: T
4.10 val qed_script: T
4.11 @@ -101,7 +100,6 @@
4.12 val thy_decl = kind "thy_decl";
4.13 val thy_load = kind "thy_load";
4.14 fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
4.15 -val thy_script = kind "thy_script";
4.16 val thy_goal = kind "thy_goal";
4.17 val qed = kind "qed";
4.18 val qed_script = kind "qed_script";
4.19 @@ -123,7 +121,7 @@
4.20
4.21 val kinds =
4.22 [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
4.23 - thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
4.24 + thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
4.25 prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
4.26 prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
4.27
4.28 @@ -249,7 +247,7 @@
4.29
4.30 val is_theory = command_category
4.31 [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
4.32 - thy_load, thy_decl, thy_script, thy_goal];
4.33 + thy_load, thy_decl, thy_goal];
4.34
4.35 val is_proof = command_category
4.36 [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
5.1 --- a/src/Pure/Isar/keyword.scala Fri Mar 14 15:26:52 2014 +0100
5.2 +++ b/src/Pure/Isar/keyword.scala Fri Mar 14 15:41:29 2014 +0100
5.3 @@ -22,7 +22,6 @@
5.4 val THY_HEADING4 = "thy_heading4"
5.5 val THY_DECL = "thy_decl"
5.6 val THY_LOAD = "thy_load"
5.7 - val THY_SCRIPT = "thy_script"
5.8 val THY_GOAL = "thy_goal"
5.9 val QED = "qed"
5.10 val QED_SCRIPT = "qed_script"
5.11 @@ -50,7 +49,7 @@
5.12 val diag = Set(DIAG)
5.13 val theory =
5.14 Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
5.15 - THY_DECL, THY_SCRIPT, THY_GOAL)
5.16 + THY_DECL, THY_GOAL)
5.17 val theory1 = Set(THY_BEGIN, THY_END)
5.18 val theory2 = Set(THY_DECL, THY_GOAL)
5.19 val proof =
5.20 @@ -61,6 +60,5 @@
5.21 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
5.22 PRF_CHAIN, PRF_DECL)
5.23 val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
5.24 - val improper = Set(THY_SCRIPT, PRF_SCRIPT)
5.25 }
5.26
6.1 --- a/src/Pure/Tools/keywords.scala Fri Mar 14 15:26:52 2014 +0100
6.2 +++ b/src/Pure/Tools/keywords.scala Fri Mar 14 15:41:29 2014 +0100
6.3 @@ -25,7 +25,6 @@
6.4 "thy_heading4" -> "theory-heading",
6.5 "thy_load" -> "theory-decl",
6.6 "thy_decl" -> "theory-decl",
6.7 - "thy_script" -> "theory-script",
6.8 "thy_goal" -> "theory-goal",
6.9 "qed_script" -> "qed",
6.10 "qed_block" -> "qed-block",
7.1 --- a/src/Tools/jEdit/src/rendering.scala Fri Mar 14 15:26:52 2014 +0100
7.2 +++ b/src/Tools/jEdit/src/rendering.scala Fri Mar 14 15:41:29 2014 +0100
7.3 @@ -53,7 +53,6 @@
7.4 import JEditToken._
7.5 Map[String, Byte](
7.6 Keyword.THY_END -> KEYWORD2,
7.7 - Keyword.THY_SCRIPT -> LABEL,
7.8 Keyword.QED_SCRIPT -> DIGIT,
7.9 Keyword.PRF_SCRIPT -> DIGIT,
7.10 Keyword.PRF_ASM -> KEYWORD3,
8.1 --- a/src/ZF/Inductive_ZF.thy Fri Mar 14 15:26:52 2014 +0100
8.2 +++ b/src/ZF/Inductive_ZF.thy Fri Mar 14 15:41:29 2014 +0100
8.3 @@ -14,8 +14,7 @@
8.4 theory Inductive_ZF
8.5 imports Fixedpt QPair Nat_ZF
8.6 keywords
8.7 - "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
8.8 - "inductive_cases" :: thy_script and
8.9 + "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
8.10 "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
8.11 "elimination" "induction" "case_eqns" "recursor_eqns"
8.12 begin