more uniform Proof_Display.print_results for theory and proof output --- avoid loss of information seen in src/Doc/JEdit/document/output-and-state.png (the first bad changeset is f8c412a45af8, see also 53b59fa42696);
(* Title: HOL/Library/Realizers.thy
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
*)
section \<open>Program extraction from proofs involving datatypes and inductive predicates\<close>
theory Realizers
imports Main
begin
ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close>
ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close>
end