src/Provers/classical.ML
changeset 4624 795b5b624c02
parent 4392 ea41d9c1b0ef
child 4625 9c6082518cfb
     1.1 --- a/src/Provers/classical.ML	Thu Feb 12 15:43:50 1998 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Feb 12 16:38:08 1998 +0100
     1.3 @@ -253,10 +253,10 @@
     1.4  
     1.5  fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
     1.6    let val pretty_thms = map Display.pretty_thm in
     1.7 -    Pretty.writeln (Pretty.big_list "introduction rules:" (pretty_thms hazIs));
     1.8      Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
     1.9 -    Pretty.writeln (Pretty.big_list "elimination rules:" (pretty_thms hazEs));
    1.10 +    Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs));
    1.11      Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs))
    1.12 +    Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs));
    1.13    end;
    1.14  
    1.15  fun rep_claset (CS args) = args;