equal
deleted
inserted
replaced
510 addsplits @{thms split_if_asm} |
510 addsplits @{thms split_if_asm} |
511 addcongs @{thms power_False_cong} |
511 addcongs @{thms power_False_cong} |
512 |
512 |
513 fun uint_arith_tacs ctxt = |
513 fun uint_arith_tacs ctxt = |
514 let |
514 let |
515 fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; |
515 fun arith_tac' n t = |
|
516 Arith_Data.verbose_arith_tac ctxt n t |
|
517 handle Cooper.COOPER _ => Seq.empty; |
516 val cs = claset_of ctxt; |
518 val cs = claset_of ctxt; |
517 val ss = simpset_of ctxt; |
519 val ss = simpset_of ctxt; |
518 in |
520 in |
519 [ clarify_tac cs 1, |
521 [ clarify_tac cs 1, |
520 full_simp_tac (uint_arith_ss_of ss) 1, |
522 full_simp_tac (uint_arith_ss_of ss) 1, |
1072 addsplits @{thms split_if_asm} |
1074 addsplits @{thms split_if_asm} |
1073 addcongs @{thms power_False_cong} |
1075 addcongs @{thms power_False_cong} |
1074 |
1076 |
1075 fun unat_arith_tacs ctxt = |
1077 fun unat_arith_tacs ctxt = |
1076 let |
1078 let |
1077 fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; |
1079 fun arith_tac' n t = |
|
1080 Arith_Data.verbose_arith_tac ctxt n t |
|
1081 handle Cooper.COOPER _ => Seq.empty; |
1078 val cs = claset_of ctxt; |
1082 val cs = claset_of ctxt; |
1079 val ss = simpset_of ctxt; |
1083 val ss = simpset_of ctxt; |
1080 in |
1084 in |
1081 [ clarify_tac cs 1, |
1085 [ clarify_tac cs 1, |
1082 full_simp_tac (unat_arith_ss_of ss) 1, |
1086 full_simp_tac (unat_arith_ss_of ss) 1, |