src/FOLP/classical.ML
changeset 32091 30e2ffbba718
parent 26928 ca87aff1ad2d
child 35762 af3ff2ba4c54
     1.1 --- a/src/FOLP/classical.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/FOLP/classical.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -124,11 +124,11 @@
     1.4  val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
     1.5  
     1.6  fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
     1.7 - (writeln"Introduction rules";  Display.prths hazIs;
     1.8 -  writeln"Safe introduction rules";  Display.prths safeIs;
     1.9 -  writeln"Elimination rules";  Display.prths hazEs;
    1.10 -  writeln"Safe elimination rules";  Display.prths safeEs;
    1.11 -  ());
    1.12 +  writeln (cat_lines
    1.13 +   (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
    1.14 +    ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
    1.15 +    ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
    1.16 +    ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
    1.17  
    1.18  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    1.19    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};