removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
authorwenzelm
Mon Jun 30 10:34:28 2014 +0200 (2014-06-30)
changeset 574422373b4c61111
parent 57441 ff534238d9b8
child 57443 577f029fde39
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/Isar_Ref/Misc.thy
src/HOL/Hoare/Arith2.thy
src/HOL/Proofs/Lambda/ParRed.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/etc/isar-keywords-ZF.el	Mon Jun 30 10:10:32 2014 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Jun 30 10:34:28 2014 +0200
     1.3 @@ -35,7 +35,6 @@
     1.4      "by"
     1.5      "cannot_undo"
     1.6      "case"
     1.7 -    "cd"
     1.8      "chapter"
     1.9      "class"
    1.10      "class_deps"
    1.11 @@ -154,7 +153,6 @@
    1.12      "print_translation"
    1.13      "proof"
    1.14      "prop"
    1.15 -    "pwd"
    1.16      "qed"
    1.17      "quit"
    1.18      "realizability"
    1.19 @@ -261,7 +259,6 @@
    1.20      "ProofGeneral\\.restart"
    1.21      "ProofGeneral\\.undo"
    1.22      "cannot_undo"
    1.23 -    "cd"
    1.24      "commit"
    1.25      "disable_pr"
    1.26      "enable_pr"
    1.27 @@ -322,7 +319,6 @@
    1.28      "print_theory"
    1.29      "print_trans_rules"
    1.30      "prop"
    1.31 -    "pwd"
    1.32      "term"
    1.33      "thm"
    1.34      "thm_deps"
     2.1 --- a/etc/isar-keywords.el	Mon Jun 30 10:10:32 2014 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon Jun 30 10:34:28 2014 +0200
     2.3 @@ -43,7 +43,6 @@
     2.4      "cartouche"
     2.5      "case"
     2.6      "case_of_simps"
     2.7 -    "cd"
     2.8      "chapter"
     2.9      "class"
    2.10      "class_deps"
    2.11 @@ -220,7 +219,6 @@
    2.12      "print_translation"
    2.13      "proof"
    2.14      "prop"
    2.15 -    "pwd"
    2.16      "qed"
    2.17      "quickcheck"
    2.18      "quickcheck_generator"
    2.19 @@ -374,7 +372,6 @@
    2.20      "ProofGeneral\\.restart"
    2.21      "ProofGeneral\\.undo"
    2.22      "cannot_undo"
    2.23 -    "cd"
    2.24      "commit"
    2.25      "disable_pr"
    2.26      "enable_pr"
    2.27 @@ -451,7 +448,6 @@
    2.28      "print_theory"
    2.29      "print_trans_rules"
    2.30      "prop"
    2.31 -    "pwd"
    2.32      "quickcheck"
    2.33      "refute"
    2.34      "sledgehammer"
     3.1 --- a/src/Doc/Isar_Ref/Misc.thy	Mon Jun 30 10:10:32 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Misc.thy	Mon Jun 30 10:34:28 2014 +0200
     3.3 @@ -112,39 +112,4 @@
     3.4    \end{description}
     3.5  *}
     3.6  
     3.7 -
     3.8 -section {* System commands *}
     3.9 -
    3.10 -text {*
    3.11 -  \begin{matharray}{rcl}
    3.12 -    @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    3.13 -    @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    3.14 -    @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    3.15 -  \end{matharray}
    3.16 -
    3.17 -  @{rail \<open>
    3.18 -    (@@{command cd} | @@{command use_thy}) @{syntax name}
    3.19 -  \<close>}
    3.20 -
    3.21 -  \begin{description}
    3.22 -
    3.23 -  \item @{command "cd"}~@{text path} changes the current directory
    3.24 -  of the Isabelle process.
    3.25 -
    3.26 -  \item @{command "pwd"} prints the current working directory.
    3.27 -
    3.28 -  \item @{command "use_thy"}~@{text A} preloads theory @{text A}.
    3.29 -  These system commands are scarcely used when working interactively,
    3.30 -  since loading of theories is done automatically as required.
    3.31 -
    3.32 -  \end{description}
    3.33 -
    3.34 -  %FIXME proper place (!?)
    3.35 -  Isabelle file specification may contain path variables (e.g.\
    3.36 -  @{verbatim "$ISABELLE_HOME"}) that are expanded accordingly.  Note
    3.37 -  that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
    3.38 -  @{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}.  The
    3.39 -  general syntax for path specifications follows POSIX conventions.
    3.40 -*}
    3.41 -
    3.42  end
     4.1 --- a/src/HOL/Hoare/Arith2.thy	Mon Jun 30 10:10:32 2014 +0200
     4.2 +++ b/src/HOL/Hoare/Arith2.thy	Mon Jun 30 10:34:28 2014 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -definition "cd" :: "[nat, nat, nat] => bool"
     4.8 +definition cd :: "[nat, nat, nat] => bool"
     4.9    where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
    4.10  
    4.11  definition gcd :: "[nat, nat] => nat"
     5.1 --- a/src/HOL/Proofs/Lambda/ParRed.thy	Mon Jun 30 10:10:32 2014 +0200
     5.2 +++ b/src/HOL/Proofs/Lambda/ParRed.thy	Mon Jun 30 10:34:28 2014 +0200
     5.3 @@ -85,7 +85,7 @@
     5.4  subsection {* Complete developments *}
     5.5  
     5.6  fun
     5.7 -  "cd" :: "dB => dB"
     5.8 +  cd :: "dB => dB"
     5.9  where
    5.10    "cd (Var n) = Var n"
    5.11  | "cd (Var n \<degree> t) = Var n \<degree> cd t"
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jun 30 10:10:32 2014 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 30 10:34:28 2014 +0200
     6.3 @@ -965,14 +965,6 @@
     6.4  (** system commands (for interactive mode only) **)
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
     6.8 -    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
     6.9 -
    6.10 -val _ =
    6.11 -  Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
    6.12 -    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
    6.13 -
    6.14 -val _ =
    6.15    Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
    6.16      (Parse.position Parse.name >>
    6.17        (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
     7.1 --- a/src/Pure/Pure.thy	Mon Jun 30 10:10:32 2014 +0200
     7.2 +++ b/src/Pure/Pure.thy	Mon Jun 30 10:34:28 2014 +0200
     7.3 @@ -88,8 +88,6 @@
     7.4      "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
     7.5      "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     7.6      "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
     7.7 -  and "cd" :: control
     7.8 -  and "pwd" :: diag
     7.9    and "use_thy" "remove_thy" "kill_thy" :: control
    7.10    and "display_drafts" "print_state" "pr" :: diag
    7.11    and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control