equal
deleted
inserted
replaced
23 | (c as @{term "Real.real :: int => _"}) $ t => |
23 | (c as @{term "Real.real :: int => _"}) $ t => |
24 abs t #>> (fn u => SOME (c $ u)) |
24 abs t #>> (fn u => SOME (c $ u)) |
25 | _ => pair NONE) |
25 | _ => pair NONE) |
26 |
26 |
27 val _ = Theory.setup (Context.theory_map ( |
27 val _ = Theory.setup (Context.theory_map ( |
28 Z3_New_Proof.add_type_parser real_type_parser #> |
28 SMT2LIB_Proof.add_type_parser real_type_parser #> |
29 Z3_New_Proof.add_term_parser real_term_parser #> |
29 SMT2LIB_Proof.add_term_parser real_term_parser #> |
30 Z3_New_Replay_Methods.add_arith_abstracter abstract)) |
30 Z3_New_Replay_Methods.add_arith_abstracter abstract)) |
31 |
31 |
32 end |
32 end |