122 |
122 |
123 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; |
123 val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; |
124 |
124 |
125 fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
125 fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) = |
126 writeln (cat_lines |
126 writeln (cat_lines |
127 (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @ |
127 (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @ |
128 ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @ |
128 ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @ |
129 ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @ |
129 ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @ |
130 ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs)); |
130 ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs)); |
131 |
131 |
132 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = |
132 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = |
133 make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; |
133 make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; |
134 |
134 |
135 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = |
135 fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = |