equal
deleted
inserted
replaced
24 fun is_positive_existential polar quant_s = |
24 fun is_positive_existential polar quant_s = |
25 (polar = Pos andalso quant_s = @{const_name Ex}) orelse |
25 (polar = Pos andalso quant_s = @{const_name Ex}) orelse |
26 (polar = Neg andalso quant_s <> @{const_name Ex}) |
26 (polar = Neg andalso quant_s <> @{const_name Ex}) |
27 |
27 |
28 val is_descr = |
28 val is_descr = |
29 member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}, |
29 member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}] |
30 @{const_name safe_Eps}] |
|
31 |
30 |
32 (** Binary coding of integers **) |
31 (** Binary coding of integers **) |
33 |
32 |
34 (* If a formula contains a numeral whose absolute value is more than this |
33 (* If a formula contains a numeral whose absolute value is more than this |
35 threshold, the unary coding is likely not to work well and we prefer the |
34 threshold, the unary coding is likely not to work well and we prefer the |