equal
deleted
inserted
replaced
43 (*the simplification procedure*) |
43 (*the simplification procedure*) |
44 fun proc ctxt ct = |
44 fun proc ctxt ct = |
45 let |
45 let |
46 val prems = Simplifier.prems_of ctxt; |
46 val prems = Simplifier.prems_of ctxt; |
47 val t = Thm.term_of ct; |
47 val t = Thm.term_of ct; |
48 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
48 val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt |
49 |
49 |
50 val (t1,t2) = Data.dest_bal t' |
50 val (t1,t2) = Data.dest_bal t' |
51 val (m1, t1') = Data.dest_coeff t1 |
51 val (m1, t1') = Data.dest_coeff t1 |
52 and (m2, t2') = Data.dest_coeff t2 |
52 and (m2, t2') = Data.dest_coeff t2 |
53 val d = (*if both are negative, also divide through by ~1*) |
53 val d = (*if both are negative, also divide through by ~1*) |