equal
deleted
inserted
replaced
26 |
26 |
27 val empty_pack = Pack([],[]); |
27 val empty_pack = Pack([],[]); |
28 |
28 |
29 fun warn_duplicates [] = [] |
29 fun warn_duplicates [] = [] |
30 | warn_duplicates dups = |
30 | warn_duplicates dups = |
31 (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups)); |
31 (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups)); |
32 dups); |
32 dups); |
33 |
33 |
34 fun (Pack(safes,unsafes)) add_safes ths = |
34 fun (Pack(safes,unsafes)) add_safes ths = |
35 let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes)) |
35 let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes)) |
36 val ths' = subtract Thm.eq_thm_prop dups ths |
36 val ths' = subtract Thm.eq_thm_prop dups ths |
49 Pack(sort (make_ord less) (safes@safes'), |
49 Pack(sort (make_ord less) (safes@safes'), |
50 sort (make_ord less) (unsafes@unsafes')); |
50 sort (make_ord less) (unsafes@unsafes')); |
51 |
51 |
52 |
52 |
53 fun print_pack (Pack(safes,unsafes)) = |
53 fun print_pack (Pack(safes,unsafes)) = |
54 (writeln "Safe rules:"; print_thms safes; |
54 (writeln "Safe rules:"; Display.print_thms safes; |
55 writeln "Unsafe rules:"; print_thms unsafes); |
55 writeln "Unsafe rules:"; Display.print_thms unsafes); |
56 |
56 |
57 (*Returns the list of all formulas in the sequent*) |
57 (*Returns the list of all formulas in the sequent*) |
58 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u |
58 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u |
59 | forms_of_seq (H $ u) = forms_of_seq u |
59 | forms_of_seq (H $ u) = forms_of_seq u |
60 | forms_of_seq _ = []; |
60 | forms_of_seq _ = []; |