148 |
148 |
149 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
149 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
150 fun mp_tac i = etac subst_prodE i THEN assume_tac i; |
150 fun mp_tac i = etac subst_prodE i THEN assume_tac i; |
151 |
151 |
152 (*"safe" when regarded as predicate calculus rules*) |
152 (*"safe" when regarded as predicate calculus rules*) |
153 val safe_brls = sort lessb |
153 val safe_brls = sort (make_ord lessb) |
154 [ (true,FE), (true,asm_rl), |
154 [ (true,FE), (true,asm_rl), |
155 (false,ProdI), (true,SumE), (true,PlusE) ]; |
155 (false,ProdI), (true,SumE), (true,PlusE) ]; |
156 |
156 |
157 val unsafe_brls = |
157 val unsafe_brls = |
158 [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), |
158 [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), |