src/FOLP/classical.ML
changeset 26928 ca87aff1ad2d
parent 17496 26535df536ae
child 32091 30e2ffbba718
equal deleted inserted replaced
26927:8684b5240f11 26928:ca87aff1ad2d
   122 (*** Manipulation of clasets ***)
   122 (*** Manipulation of clasets ***)
   123 
   123 
   124 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
   124 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
   125 
   125 
   126 fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   126 fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   127  (writeln"Introduction rules";  prths hazIs;
   127  (writeln"Introduction rules";  Display.prths hazIs;
   128   writeln"Safe introduction rules";  prths safeIs;
   128   writeln"Safe introduction rules";  Display.prths safeIs;
   129   writeln"Elimination rules";  prths hazEs;
   129   writeln"Elimination rules";  Display.prths hazEs;
   130   writeln"Safe elimination rules";  prths safeEs;
   130   writeln"Safe elimination rules";  Display.prths safeEs;
   131   ());
   131   ());
   132 
   132 
   133 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
   133 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
   134   make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
   134   make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
   135 
   135