equal
deleted
inserted
replaced
23 |
23 |
24 val true_tm = @{cterm "True"}; |
24 val true_tm = @{cterm "True"}; |
25 val false_tm = @{cterm "False"}; |
25 val false_tm = @{cterm "False"}; |
26 val zdvd1_eq = @{thm "zdvd1_eq"}; |
26 val zdvd1_eq = @{thm "zdvd1_eq"}; |
27 val presburger_ss = @{simpset} addsimps [zdvd1_eq]; |
27 val presburger_ss = @{simpset} addsimps [zdvd1_eq]; |
28 val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::zadd_ac); |
28 val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac}); |
29 (* Some types and constants *) |
29 (* Some types and constants *) |
30 val iT = HOLogic.intT |
30 val iT = HOLogic.intT |
31 val bT = HOLogic.boolT; |
31 val bT = HOLogic.boolT; |
32 val dest_numeral = HOLogic.dest_number #> snd; |
32 val dest_numeral = HOLogic.dest_number #> snd; |
33 |
33 |