# HG changeset patch
# User wenzelm
# Date 1404117268 -7200
# Node ID 2373b4c611114cb9fa9794643fbcbbdb6a61776e
# Parent  ff534238d9b89f10867853dd9cd5de32fb2de04f
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;

diff -r ff534238d9b8 -r 2373b4c61111 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Jun 30 10:10:32 2014 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Jun 30 10:34:28 2014 +0200
@@ -35,7 +35,6 @@
     "by"
     "cannot_undo"
     "case"
-    "cd"
     "chapter"
     "class"
     "class_deps"
@@ -154,7 +153,6 @@
     "print_translation"
     "proof"
     "prop"
-    "pwd"
     "qed"
     "quit"
     "realizability"
@@ -261,7 +259,6 @@
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
     "cannot_undo"
-    "cd"
     "commit"
     "disable_pr"
     "enable_pr"
@@ -322,7 +319,6 @@
     "print_theory"
     "print_trans_rules"
     "prop"
-    "pwd"
     "term"
     "thm"
     "thm_deps"
diff -r ff534238d9b8 -r 2373b4c61111 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Jun 30 10:10:32 2014 +0200
+++ b/etc/isar-keywords.el	Mon Jun 30 10:34:28 2014 +0200
@@ -43,7 +43,6 @@
     "cartouche"
     "case"
     "case_of_simps"
-    "cd"
     "chapter"
     "class"
     "class_deps"
@@ -220,7 +219,6 @@
     "print_translation"
     "proof"
     "prop"
-    "pwd"
     "qed"
     "quickcheck"
     "quickcheck_generator"
@@ -374,7 +372,6 @@
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
     "cannot_undo"
-    "cd"
     "commit"
     "disable_pr"
     "enable_pr"
@@ -451,7 +448,6 @@
     "print_theory"
     "print_trans_rules"
     "prop"
-    "pwd"
     "quickcheck"
     "refute"
     "sledgehammer"
diff -r ff534238d9b8 -r 2373b4c61111 src/Doc/Isar_Ref/Misc.thy
--- a/src/Doc/Isar_Ref/Misc.thy	Mon Jun 30 10:10:32 2014 +0200
+++ b/src/Doc/Isar_Ref/Misc.thy	Mon Jun 30 10:34:28 2014 +0200
@@ -112,39 +112,4 @@
   \end{description}
 *}
 
-
-section {* System commands *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
-    @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
-    @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
-  \end{matharray}
-
-  @{rail \<open>
-    (@@{command cd} | @@{command use_thy}) @{syntax name}
-  \<close>}
-
-  \begin{description}
-
-  \item @{command "cd"}~@{text path} changes the current directory
-  of the Isabelle process.
-
-  \item @{command "pwd"} prints the current working directory.
-
-  \item @{command "use_thy"}~@{text A} preloads theory @{text A}.
-  These system commands are scarcely used when working interactively,
-  since loading of theories is done automatically as required.
-
-  \end{description}
-
-  %FIXME proper place (!?)
-  Isabelle file specification may contain path variables (e.g.\
-  @{verbatim "$ISABELLE_HOME"}) that are expanded accordingly.  Note
-  that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
-  @{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}.  The
-  general syntax for path specifications follows POSIX conventions.
-*}
-
 end
diff -r ff534238d9b8 -r 2373b4c61111 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Mon Jun 30 10:10:32 2014 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Mon Jun 30 10:34:28 2014 +0200
@@ -9,7 +9,7 @@
 imports Main
 begin
 
-definition "cd" :: "[nat, nat, nat] => bool"
+definition cd :: "[nat, nat, nat] => bool"
   where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
 
 definition gcd :: "[nat, nat] => nat"
diff -r ff534238d9b8 -r 2373b4c61111 src/HOL/Proofs/Lambda/ParRed.thy
--- a/src/HOL/Proofs/Lambda/ParRed.thy	Mon Jun 30 10:10:32 2014 +0200
+++ b/src/HOL/Proofs/Lambda/ParRed.thy	Mon Jun 30 10:34:28 2014 +0200
@@ -85,7 +85,7 @@
 subsection {* Complete developments *}
 
 fun
-  "cd" :: "dB => dB"
+  cd :: "dB => dB"
 where
   "cd (Var n) = Var n"
 | "cd (Var n \<degree> t) = Var n \<degree> cd t"
diff -r ff534238d9b8 -r 2373b4c61111 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 30 10:10:32 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 30 10:34:28 2014 +0200
@@ -965,14 +965,6 @@
 (** system commands (for interactive mode only) **)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
-    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
-
-val _ =
-  Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
-    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
-
-val _ =
   Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
     (Parse.position Parse.name >>
       (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
diff -r ff534238d9b8 -r 2373b4c61111 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jun 30 10:10:32 2014 +0200
+++ b/src/Pure/Pure.thy	Mon Jun 30 10:34:28 2014 +0200
@@ -88,8 +88,6 @@
     "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
-  and "cd" :: control
-  and "pwd" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
   and "display_drafts" "print_state" "pr" :: diag
   and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control