discontinued redundant 'use' command;
authorwenzelm
Wed Feb 27 17:32:17 2013 +0100 (2013-02-27)
changeset 5129571fc3776c453
parent 51294 0850d43cb355
child 51296 77e71d54efda
discontinued redundant 'use' command;
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/IsarImplementation/ML.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Wed Feb 27 16:27:44 2013 +0100
     1.2 +++ b/NEWS	Wed Feb 27 17:32:17 2013 +0100
     1.3 @@ -10,6 +10,9 @@
     1.4  commands like 'ML_file' work without separate declaration of file
     1.5  dependencies.  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Discontinued redundant 'use' command, which was superseded by
     1.8 +'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  
     2.1 --- a/etc/isar-keywords-ZF.el	Wed Feb 27 16:27:44 2013 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Wed Feb 27 17:32:17 2013 +0100
     2.3 @@ -200,7 +200,6 @@
     2.4      "undos_proof"
     2.5      "unfolding"
     2.6      "unused_thms"
     2.7 -    "use"
     2.8      "use_thy"
     2.9      "using"
    2.10      "welcome"
    2.11 @@ -407,8 +406,7 @@
    2.12      "type_notation"
    2.13      "type_synonym"
    2.14      "typed_print_translation"
    2.15 -    "typedecl"
    2.16 -    "use"))
    2.17 +    "typedecl"))
    2.18  
    2.19  (defconst isar-keywords-theory-script
    2.20    '("inductive_cases"))
     3.1 --- a/etc/isar-keywords.el	Wed Feb 27 16:27:44 2013 +0100
     3.2 +++ b/etc/isar-keywords.el	Wed Feb 27 17:32:17 2013 +0100
     3.3 @@ -288,7 +288,6 @@
     3.4      "undos_proof"
     3.5      "unfolding"
     3.6      "unused_thms"
     3.7 -    "use"
     3.8      "use_thy"
     3.9      "using"
    3.10      "value"
    3.11 @@ -573,8 +572,7 @@
    3.12      "type_notation"
    3.13      "type_synonym"
    3.14      "typed_print_translation"
    3.15 -    "typedecl"
    3.16 -    "use"))
    3.17 +    "typedecl"))
    3.18  
    3.19  (defconst isar-keywords-theory-script
    3.20    '("inductive_cases"
     4.1 --- a/src/Doc/IsarImplementation/ML.thy	Wed Feb 27 16:27:44 2013 +0100
     4.2 +++ b/src/Doc/IsarImplementation/ML.thy	Wed Feb 27 17:32:17 2013 +0100
     4.3 @@ -540,7 +540,7 @@
     4.4  
     4.5  text {* The primary Isar source language provides facilities to ``open
     4.6    a window'' to the underlying ML compiler.  Especially see the Isar
     4.7 -  commands @{command_ref "use"} and @{command_ref "ML"}: both work the
     4.8 +  commands @{command_ref "ML_file"} and @{command_ref "ML"}: both work the
     4.9    same way, only the source text is provided via a file vs.\ inlined,
    4.10    respectively.  Apart from embedding ML into the main theory
    4.11    definition like that, there are many more commands that refer to ML
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Feb 27 16:27:44 2013 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 27 17:32:17 2013 +0100
     5.3 @@ -270,13 +270,6 @@
     5.4  (* use ML text *)
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.command @{command_spec "use"} "ML text from file"
     5.8 -    (Parse.path >> (fn name =>
     5.9 -      Toplevel.generic_theory (fn gthy =>
    5.10 -        (legacy_feature "Old 'use' command -- use 'ML_file' instead";
    5.11 -         Thy_Load.exec_ml (Path.explode name) gthy))));
    5.12 -
    5.13 -val _ =
    5.14    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
    5.15      (Parse.ML_source >> (fn (txt, pos) =>
    5.16        Toplevel.generic_theory
     6.1 --- a/src/Pure/Pure.thy	Wed Feb 27 16:27:44 2013 +0100
     6.2 +++ b/src/Pure/Pure.thy	Wed Feb 27 17:32:17 2013 +0100
     6.3 @@ -29,7 +29,7 @@
     6.4      "abbreviation" "type_notation" "no_type_notation" "notation"
     6.5      "no_notation" "axiomatization" "theorems" "lemmas" "declare"
     6.6      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
     6.7 -  and "use" "ML" :: thy_decl % "ML"
     6.8 +  and "ML" :: thy_decl % "ML"
     6.9    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    6.10    and "ML_val" "ML_command" :: diag % "ML"
    6.11    and "setup" "local_setup" "attribute_setup" "method_setup"