# HG changeset patch
# User wenzelm
# Date 964715155 -7200
# Node ID ea80449107cc7cae8620dbd5acdeecb1b78f7be6
# Parent  4b37161f2b2ed907e79b62170fa2cc66e1bee3b0
added thm_deps;

diff -r 4b37161f2b2e -r ea80449107cc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Jul 27 18:25:44 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jul 27 18:25:55 2000 +0200
@@ -51,6 +51,7 @@
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
   val print_thms_containing: xstring list -> Toplevel.transition -> Toplevel.transition
+  val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_lthms: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
@@ -178,6 +179,9 @@
 fun print_thms_containing cs = Toplevel.keep (fn state =>
   ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
 
+fun thm_deps args = Toplevel.keep (fn state =>
+  ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
+
 
 (* print proof context contents *)
 
@@ -215,7 +219,7 @@
   in with_modes ms (fn () => Pretty.string_of (Pretty.quote (Sign.pretty_typ sign T))) end;
 
 fun print_item string_of (x, y) = Toplevel.keep (fn state =>
-  writeln (string_of (Toplevel.node_case Proof.init_state Proof.enter_forward state) x y));
+  writeln (string_of (Toplevel.enter_forward_proof state) x y));
 
 val print_thms = print_item string_of_thms;
 val print_prop = print_item string_of_prop;
diff -r 4b37161f2b2e -r ea80449107cc src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 27 18:25:44 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 27 18:25:55 2000 +0200
@@ -538,6 +538,10 @@
   OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
     K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
 
+val thm_depsP =
+  OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
+    K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
+
 val print_bindsP =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
@@ -683,8 +687,8 @@
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP,
   print_trans_rulesP, print_methodsP, print_antiquotationsP,
-  thms_containingP, print_bindsP, print_lthmsP, print_casesP,
-  print_thmsP, print_propP, print_termP, print_typeP,
+  thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
+  print_casesP, print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,