equal
deleted
inserted
replaced
279 i = subgoal *) |
279 i = subgoal *) |
280 |
280 |
281 fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st => |
281 fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st => |
282 let |
282 let |
283 val g = List.nth (prems_of st, i - 1) |
283 val g = List.nth (prems_of st, i - 1) |
284 val sg = sign_of_thm st |
284 val sg = Thm.theory_of_thm st |
285 (* The Abstraction step *) |
285 (* The Abstraction step *) |
286 val g' = if a then abstract_pres sg g else g |
286 val g' = if a then abstract_pres sg g else g |
287 (* Transform the term*) |
287 (* Transform the term*) |
288 val (t,np,nh) = prepare_for_presburger sg q g' |
288 val (t,np,nh) = prepare_for_presburger sg q g' |
289 (* Some simpsets for dealing with mod div abs and nat*) |
289 (* Some simpsets for dealing with mod div abs and nat*) |