# HG changeset patch # User wenzelm # Date 955973404 -7200 # Node ID 71acc2d8991a7ad81960fe155a5f60329d9e1b95 # Parent 7b15f4bdd72fab027d9bf8dbfebb8d746a5b4cda Pretty.chunks; diff -r 7b15f4bdd72f -r 71acc2d8991a src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Apr 17 14:08:51 2000 +0200 +++ b/src/Provers/classical.ML Mon Apr 17 14:10:04 2000 +0200 @@ -270,12 +270,13 @@ fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = let val pretty_thms = map Display.pretty_thm in - Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); - Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); - Pretty.writeln (Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs)); - Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); - Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)); - Pretty.writeln (Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)) + [Pretty.big_list "safe introduction rules:" (pretty_thms safeIs), + Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs), + Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs), + Pretty.big_list "safe elimination rules:" (pretty_thms safeEs), + Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs), + Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)] + |> Pretty.chunks |> Pretty.writeln end; fun rep_cs (CS args) = args; diff -r 7b15f4bdd72f -r 71acc2d8991a src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Mon Apr 17 14:08:51 2000 +0200 +++ b/src/Provers/simplifier.ML Mon Apr 17 14:10:04 2000 +0200 @@ -170,9 +170,10 @@ fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss); in - Pretty.writeln (Pretty.big_list "simplification rules:" (pretty_thms simps)); - Pretty.writeln (Pretty.big_list "simplification procedures:" (map pretty_proc procs)); - Pretty.writeln (Pretty.big_list "congruences:" (pretty_thms congs)) + [Pretty.big_list "simplification rules:" (pretty_thms simps), + Pretty.big_list "simplification procedures:" (map pretty_proc procs), + Pretty.big_list "congruences:" (pretty_thms congs)] + |> Pretty.chunks |> Pretty.writeln end;