# HG changeset patch
# User wenzelm
# Date 952534465 -3600
# Node ID 1c833efb2802b7830f5017d40fbabbba37a20c35
# Parent  bdc3ee0d8cb613e72698a4719f77de8f43a454a6
added print_cases;

diff -r bdc3ee0d8cb6 -r 1c833efb2802 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 08 17:52:38 2000 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 08 17:54:25 2000 +0100
@@ -44,6 +44,7 @@
   val print_thms_containing: xstring 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
   val print_thms: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_prop: string -> Toplevel.transition -> Toplevel.transition
   val print_term: string -> Toplevel.transition -> Toplevel.transition
@@ -151,6 +152,7 @@
 
 val print_binds = Toplevel.keep (ProofContext.print_binds o Proof.context_of o Toplevel.proof_of);
 val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of);
+val print_cases = Toplevel.keep (ProofContext.print_cases o Proof.context_of o Toplevel.proof_of);
 
 
 (* print theorems / types / terms / props *)