src/Pure/Pure.thy
changeset 58846 98c03412079b
parent 58845 8451eddc4d67
child 58860 fee7cfa69c50
--- a/src/Pure/Pure.thy	Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/Pure.thy	Fri Oct 31 16:03:45 2014 +0100
@@ -88,11 +88,8 @@
     "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
-  and "use_thy" "remove_thy" "kill_thy" :: control
   and "display_drafts" "print_state" :: diag
-  and "commit" "quit" "exit" :: control
   and "welcome" :: diag
-  and "init_toplevel" "linear_undo" "undo" "undos_proof" "kill" :: control
   and "end" :: thy_end % "theory"
   and "realizers" :: thy_decl == ""
   and "realizability" :: thy_decl == ""