src/FOLP/classical.ML
changeset 32091 30e2ffbba718
parent 26928 ca87aff1ad2d
child 35762 af3ff2ba4c54
equal deleted inserted replaced
32090:39acf19e9f3a 32091:30e2ffbba718
   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";  Display.prths hazIs;
   127   writeln (cat_lines
   128   writeln"Safe introduction rules";  Display.prths safeIs;
   128    (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
   129   writeln"Elimination rules";  Display.prths hazEs;
   129     ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
   130   writeln"Safe elimination rules";  Display.prths safeEs;
   130     ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
   131   ());
   131     ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
   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 
   136 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths =
   136 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths =