discontinued somewhat pointless "thy_script" keyword kind;
authorwenzelm
Fri Mar 14 15:41:29 2014 +0100 (2014-03-14)
changeset 561468453d35e4684
parent 56145 a200bffe4027
child 56147 9589605bcf41
discontinued somewhat pointless "thy_script" keyword kind;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/HOL/Inductive.thy
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Tools/keywords.scala
src/Tools/jEdit/src/rendering.scala
src/ZF/Inductive_ZF.thy
     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