equal
deleted
inserted
replaced
29 |
29 |
30 |
30 |
31 (* Invoking the oracle *) |
31 (* Invoking the oracle *) |
32 |
32 |
33 fun pres_oracle sg t = |
33 fun pres_oracle sg t = |
34 invoke_oracle (the_context()) "presburger_oracle" |
34 invoke_oracle (theory "Presburger") "presburger_oracle" |
35 (sg, CooperDec.COOPER_ORACLE t) ; |
35 (sg, CooperDec.COOPER_ORACLE t) ; |
36 |
36 |
37 val presburger_ss = simpset_of (theory "Presburger"); |
37 val presburger_ss = simpset_of (theory "Presburger"); |
38 |
38 |
39 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |
39 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |