equal
deleted
inserted
replaced
75 |
75 |
76 fun choose_logic ctxt ts = |
76 fun choose_logic ctxt ts = |
77 let |
77 let |
78 fun choose [] = "AUFLIA" |
78 fun choose [] = "AUFLIA" |
79 | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs) |
79 | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs) |
80 in "(set-logic " ^ choose (Logics.get (Context.Proof ctxt)) ^ ")\n" end |
80 in |
|
81 (case choose (Logics.get (Context.Proof ctxt)) of |
|
82 "" => "" (* for default Z3 logic, a subset of everything *) |
|
83 | logic => "(set-logic " ^ logic ^ ")\n") |
|
84 end |
81 |
85 |
82 |
86 |
83 (** serialization **) |
87 (** serialization **) |
84 |
88 |
85 fun var i = "?v" ^ string_of_int i |
89 fun var i = "?v" ^ string_of_int i |