equal
deleted
inserted
replaced
1549 |> fold Simplifier.add_cong @{thms power_False_cong} |
1549 |> fold Simplifier.add_cong @{thms power_False_cong} |
1550 |
1550 |
1551 fun uint_arith_tacs ctxt = |
1551 fun uint_arith_tacs ctxt = |
1552 let |
1552 let |
1553 fun arith_tac' n t = |
1553 fun arith_tac' n t = |
1554 Arith_Data.verbose_arith_tac ctxt n t |
1554 Arith_Data.arith_tac ctxt n t |
1555 handle Cooper.COOPER _ => Seq.empty; |
1555 handle Cooper.COOPER _ => Seq.empty; |
1556 in |
1556 in |
1557 [ clarify_tac ctxt 1, |
1557 [ clarify_tac ctxt 1, |
1558 full_simp_tac (uint_arith_simpset ctxt) 1, |
1558 full_simp_tac (uint_arith_simpset ctxt) 1, |
1559 ALLGOALS (full_simp_tac |
1559 ALLGOALS (full_simp_tac |
2051 |> fold Simplifier.add_cong @{thms power_False_cong} |
2051 |> fold Simplifier.add_cong @{thms power_False_cong} |
2052 |
2052 |
2053 fun unat_arith_tacs ctxt = |
2053 fun unat_arith_tacs ctxt = |
2054 let |
2054 let |
2055 fun arith_tac' n t = |
2055 fun arith_tac' n t = |
2056 Arith_Data.verbose_arith_tac ctxt n t |
2056 Arith_Data.arith_tac ctxt n t |
2057 handle Cooper.COOPER _ => Seq.empty; |
2057 handle Cooper.COOPER _ => Seq.empty; |
2058 in |
2058 in |
2059 [ clarify_tac ctxt 1, |
2059 [ clarify_tac ctxt 1, |
2060 full_simp_tac (unat_arith_simpset ctxt) 1, |
2060 full_simp_tac (unat_arith_simpset ctxt) 1, |
2061 ALLGOALS (full_simp_tac |
2061 ALLGOALS (full_simp_tac |