src/Pure/Isar/proof_context.ML
changeset 6870 43d64c520d11
parent 6852 fe39a3054d82
child 6875 df31250ccb3a
equal deleted inserted replaced
6869:850812ed9976 6870:43d64c520d11
   139 
   139 
   140 
   140 
   141 (* local theorems *)
   141 (* local theorems *)
   142 
   142 
   143 fun strings_of_thms (Context {thms, ...}) =
   143 fun strings_of_thms (Context {thms, ...}) =
   144   strings_of_items Display.pretty_thm "Local theorems:" (Symtab.dest thms);
   144   strings_of_items (setmp Display.show_hyps false Display.pretty_thm)
       
   145     "Local theorems:" (Symtab.dest thms);
   145 
   146 
   146 val print_thms = seq writeln o strings_of_thms;
   147 val print_thms = seq writeln o strings_of_thms;
   147 
   148 
   148 
   149 
   149 (* main context *)
   150 (* main context *)