equal
deleted
inserted
replaced
123 let |
123 let |
124 fun err_if b msg = if b then raise Proof.STATE (msg, state) else (); |
124 fun err_if b msg = if b then raise Proof.STATE (msg, state) else (); |
125 val facts = Proof.the_facts state; |
125 val facts = Proof.the_facts state; |
126 val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state); |
126 val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state); |
127 |
127 |
128 fun differ thms thms' = not (Library.equal_lists Thm.eq_thm (thms, thms')); |
128 val eq_prop = op aconv o pairself (#prop o Thm.rep_thm); |
|
129 fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms')); |
129 fun combine thms = |
130 fun combine thms = |
130 Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules)); |
131 Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules)); |
131 |
132 |
132 val (initial, calculations) = |
133 val (initial, calculations) = |
133 (case get_calculation state of |
134 (case get_calculation state of |