# HG changeset patch
# User blanchet
# Date 1402527649 -7200
# Node ID 489083abce44a51043ad64378d67c696a756ca87
# Parent  d52012eabf0d468a635e8c841d5a45587933811d
tuning

diff -r d52012eabf0d -r 489083abce44 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
 
 theory SMT
-imports List
+imports ATP
 keywords "smt_status" :: diag
 begin
 
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_builtin.ML
--- a/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -40,7 +40,7 @@
   val dest_builtin_ext: Proof.context -> string * typ -> term list -> term list option
   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
   val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
-end
+end;
 
 structure SMT2_Builtin: SMT2_BUILTIN =
 struct
@@ -219,4 +219,4 @@
 
 fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_config.ML
--- a/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -47,7 +47,7 @@
 
   (*setup*)
   val print_setup: Proof.context -> unit
-end
+end;
 
 structure SMT2_Config: SMT2_CONFIG =
 struct
@@ -246,4 +246,4 @@
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_datatypes.ML
--- a/src/HOL/Tools/SMT2/smt2_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -10,7 +10,7 @@
   val add_decls: typ ->
     (typ * (term * term list) list) list list * Proof.context ->
     (typ * (term * term list) list) list list * Proof.context
-end
+end;
 
 structure SMT2_Datatypes: SMT2_DATATYPES =
 struct
@@ -90,4 +90,4 @@
             in fold add Us (ins dss, ctxt2) end))
   in add T ([], ctxt) |>> append declss o map snd end
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_failure.ML
--- a/src/HOL/Tools/SMT2/smt2_failure.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_failure.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -14,7 +14,7 @@
     Other_Failure of string
   val string_of_failure: failure -> string
   exception SMT of failure
-end
+end;
 
 structure SMT2_Failure: SMT2_FAILURE =
 struct
@@ -37,4 +37,4 @@
 
 exception SMT of failure
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_normalize.ML
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -16,7 +16,7 @@
   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
   val normalize: Proof.context -> thm list -> (int * thm) list
-end
+end;
 
 structure SMT2_Normalize: SMT2_NORMALIZE =
 struct
@@ -264,7 +264,6 @@
 fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
 
 
-
 (* unfolding of definitions and theory-specific rewritings *)
 
 fun expand_head_conv cv ct =
@@ -456,7 +455,6 @@
   |> burrow_ids add_nat_embedding
 
 
-
 (* overall normalization *)
 
 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
@@ -526,4 +524,4 @@
   setup_abs_min_max #>
   setup_nat_as_int))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_real.ML
--- a/src/HOL/Tools/SMT2/smt2_real.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_real.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -118,4 +118,4 @@
   Z3_New_Interface.add_mk_builtins z3_mk_builtins #>
   Z3_New_Replay_Util.add_simproc real_linarith_proc))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -38,12 +38,11 @@
   (*tactic*)
   val smt2_tac: Proof.context -> thm list -> int -> tactic
   val smt2_tac': Proof.context -> thm list -> int -> tactic
-end
+end;
 
 structure SMT2_Solver: SMT2_SOLVER =
 struct
 
-
 (* interface to external solvers *)
 
 local
@@ -298,4 +297,4 @@
 
 end
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -12,7 +12,7 @@
     Z3_Non_Commercial_Declined
   val z3_non_commercial: unit -> z3_non_commercial
   val z3_extensions: bool Config.T
-end
+end;
 
 structure SMT2_Systems: SMT2_SYSTEMS =
 struct
@@ -155,4 +155,4 @@
   SMT2_Solver.add_solver yices #>
   SMT2_Solver.add_solver z3)
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_translate.ML
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -35,7 +35,7 @@
   (*translation*)
   val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
   val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
-end
+end;
 
 structure SMT2_Translate: SMT2_TRANSLATE =
 struct
@@ -54,7 +54,6 @@
   SQua of squant * string list * sterm spattern list * sterm
 
 
-
 (* translation configuration *)
 
 type sign = {
@@ -76,7 +75,6 @@
   assms: (int * thm) list }
 
 
-
 (* translation context *)
 
 fun add_components_of_typ (Type (s, Ts)) =
@@ -131,7 +129,6 @@
   end
 
 
-
 (* preprocessing *)
 
 (** datatype declarations **)
@@ -454,7 +451,6 @@
   in ((sign_of (header ts) dtyps trx', us), trx') end
 
 
-
 (* translation *)
 
 structure Configs = Generic_Data
@@ -521,4 +517,4 @@
     ||> replay_data_of ctxt2 rewrite_rules ithms
   end
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smt2_util.ML
--- a/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -59,7 +59,7 @@
   val under_quant_conv: (Proof.context * cterm list -> conv) ->
     Proof.context -> conv
   val prop_conv: conv -> conv
-end
+end;
 
 structure SMT2_Util: SMT2_UTIL =
 struct
@@ -221,4 +221,4 @@
     @{const Trueprop} $ _ => Conv.arg_conv cv ct
   | _ => raise CTERM ("not a property", [ct]))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smtlib2.ML
--- a/src/HOL/Tools/SMT2/smtlib2.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -17,7 +17,7 @@
   val parse: string list -> tree
   val pretty_tree: tree -> Pretty.T
   val str_of: tree -> string
-end
+end;
 
 structure SMTLIB2: SMTLIB2 =
 struct
@@ -37,7 +37,6 @@
 datatype unfinished = None | String of string | Symbol of string
 
 
-
 (* utilities *)
 
 fun read_raw pred l cs =
@@ -47,7 +46,6 @@
   | x => x)
 
 
-
 (* numerals and decimals *)
 
 fun int_of cs = fst (read_int cs)
@@ -60,7 +58,6 @@
   | (cs1, cs2) => (Num (int_of cs1), cs2))
 
 
-
 (* binary numbers *)
 
 fun is_bin c = (c = "0" orelse c = "1")
@@ -68,7 +65,6 @@
 fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
 
 
-
 (* hex numbers *)
 
 val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
@@ -85,7 +81,6 @@
 fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
 
 
-
 (* symbols *)
 
 val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-" 
@@ -98,7 +93,6 @@
 fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
 
 
-
 (* quoted tokens *)
 
 fun read_quoted stop (escape, replacement) cs =
@@ -116,7 +110,6 @@
 fun read_symbol cs = read_quoted ["|"] ([], "") cs
 
 
-
 (* core parser *)
 
 fun read _ [] rest tss = (rest, tss)
@@ -172,7 +165,6 @@
 fun parse lines = finish (fold add_line lines (1, (None, [[]])))
 
 
-
 (* pretty printer *)
 
 fun pretty_tree (Num i) = Pretty.str (string_of_int i)
@@ -196,4 +188,4 @@
 
 val str_of = Pretty.str_of o pretty_tree
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/smtlib2_interface.ML
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -11,7 +11,7 @@
   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
   val translate_config: Proof.context -> SMT2_Translate.config
   val assert_index_of_name: string -> int
-end
+end;
 
 structure SMTLIB2_Interface: SMTLIB2_INTERFACE =
 struct
@@ -156,4 +156,4 @@
   (setup_builtins #>
    SMT2_Translate.add_config (smtlib2C, translate_config)))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_interface.ML
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -19,7 +19,7 @@
   val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
 
   val is_builtin_theory_term: Proof.context -> term -> bool
-end
+end;
 
 structure Z3_New_Interface: Z3_NEW_INTERFACE =
 struct
@@ -27,7 +27,6 @@
 val smtlib2_z3C = SMTLIB2_Interface.smtlib2C @ ["z3"]
 
 
-
 (* interface *)
 
 local
@@ -63,7 +62,6 @@
 end
 
 
-
 (* constructors *)
 
 datatype sym = Sym of string * sym list
@@ -185,7 +183,6 @@
     | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
 
 
-
 (* abstraction *)
 
 fun is_builtin_theory_term ctxt t =
@@ -195,4 +192,4 @@
       (Const c, ts) => SMT2_Builtin.is_builtin_fun ctxt c ts
     | _ => false)
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_proof.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -194,7 +194,6 @@
            error (msg ^ ": " ^ SMTLIB2.str_of t)
 
 
-
 (* handling of bound variables *)
 
 fun subst_of tyenv =
@@ -269,7 +268,6 @@
   end
 
 
-
 (* linearizing proofs and resolving types of bound variables *)
 
 fun has_step (tab, _) = Inttab.defined tab
@@ -300,7 +298,6 @@
   rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
 
 
-
 (* overall proof parser *)
 
 fun parse typs funs lines ctxt =
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_real.ML
--- a/src/HOL/Tools/SMT2/z3_new_real.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_real.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -29,4 +29,4 @@
   SMTLIB2_Proof.add_term_parser real_term_parser #>
   Z3_New_Replay_Methods.add_arith_abstracter abstract))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -11,7 +11,7 @@
     ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
     SMT2_Solver.parsed_proof
   val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> thm
-end
+end;
 
 structure Z3_New_Replay: Z3_NEW_REPLAY =
 struct
@@ -216,4 +216,4 @@
     Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
   end
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_replay_literals.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -28,13 +28,11 @@
   val explode: bool -> bool -> bool -> term list -> thm -> thm list
   val join: bool -> littab -> term -> thm
   val prove_conj_disj_eq: cterm -> thm
-end
+end;
 
 structure Z3_New_Replay_Literals: Z3_NEW_REPLAY_LITERALS =
 struct
 
-
-
 (* literal table *)
 
 type littab = thm Termtab.table
@@ -48,14 +46,12 @@
   Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
 
 
-
 (* rules *)
 
 val true_thm = @{lemma "~False" by simp}
 val rewrite_true = @{lemma "True == ~ False" by simp}
 
 
-
 (* properties and term operations *)
 
 val is_neg = (fn @{const Not} $ _ => true | _ => false)
@@ -84,7 +80,6 @@
 val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not})
 
 
-
 (* proof tools *)
 
 (** explosion of conjunctions and disjunctions **)
@@ -353,4 +348,4 @@
 
 end
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -50,7 +50,7 @@
   val mp_oeq: z3_method
   val th_lemma: string -> z3_method
   val method_for: Z3_New_Proof.z3_rule -> z3_method
-end
+end;
 
 structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
 struct
@@ -58,7 +58,6 @@
 type z3_method = Proof.context -> thm list -> term -> thm
 
 
-
 (* utility functions *)
 
 fun trace ctxt f = SMT2_Config.trace_msg ctxt f ()
@@ -144,7 +143,6 @@
 fun quant_tac ctxt = Blast.blast_tac ctxt
 
 
-
 (* plug-ins *)
 
 type abs_context = int * term Termtab.table
@@ -174,7 +172,6 @@
 fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
 
 
-
 (* abstraction *)
 
 fun prove_abstract ctxt thms t tac f =
@@ -279,13 +276,11 @@
   in abs u end
 
 
-
 (* truth axiom *)
 
 fun true_axiom _ _ _ = @{thm TrueI}
 
 
-
 (* modus ponens *)
 
 fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
@@ -294,27 +289,23 @@
 val mp_oeq = mp
 
 
-
 (* reflexivity *)
 
 fun refl ctxt _ t = match_instantiate ctxt t @{thm refl}
 
 
-
 (* symmetry *)
 
 fun symm _ [thm] _ = thm RS @{thm sym}
   | symm ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Reflexivity thms t
 
 
-
 (* transitivity *)
 
 fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans}))
   | trans ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Transitivity thms t
 
 
-
 (* congruence *)
 
 fun ctac prems i st = st |> (
@@ -345,7 +336,6 @@
   ("full", cong_full ctxt thms)] thms
 
 
-
 (* quantifier introduction *)
 
 val quant_intro_rules = @{lemma
@@ -360,7 +350,6 @@
   | quant_intro ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Quant_Intro thms t
 
 
-
 (* distributivity of conjunctions and disjunctions *)
 
 (* TODO: there are no tests with this proof rule *)
@@ -368,7 +357,6 @@
   prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
 
 
-
 (* elimination of conjunctions *)
 
 fun and_elim ctxt [thm] t =
@@ -379,7 +367,6 @@
   | and_elim ctxt thms t = replay_rule_error ctxt Z3_New_Proof.And_Elim thms t
 
 
-
 (* elimination of negated disjunctions *)
 
 fun not_or_elim ctxt [thm] t =
@@ -391,7 +378,6 @@
       replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t
 
 
-
 (* rewriting *)
 
 local
@@ -452,19 +438,16 @@
 fun rewrite_star ctxt = rewrite ctxt
 
 
-
 (* pulling quantifiers *)
 
 fun pull_quant ctxt _ t = prove ctxt t quant_tac
 
 
-
 (* pushing quantifiers *)
 
 fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *)
 
 
-
 (* elimination of unused bound variables *)
 
 val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
@@ -480,13 +463,11 @@
 fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
 
 
-
 (* destructive equality resolution *)
 
 fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *)
 
 
-
 (* quantifier instantiation *)
 
 val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
@@ -496,7 +477,6 @@
   THEN' rtac @{thm excluded_middle})
 
 
-
 (* propositional lemma *)
 
 exception LEMMA of unit
@@ -535,7 +515,6 @@
   | lemma ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Lemma thms t
 
 
-
 (* unit resolution *)
 
 fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
@@ -553,7 +532,6 @@
     (fn (prems, concl) => (prems, concl)))
 
 
-
 (* iff-true *)
 
 val iff_true_rule = @{lemma "P ==> P = True" by fast}
@@ -562,7 +540,6 @@
   | iff_true ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_True thms t
 
 
-
 (* iff-false *)
 
 val iff_false_rule = @{lemma "~P ==> P = False" by fast}
@@ -571,13 +548,11 @@
   | iff_false ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_False thms t
 
 
-
 (* commutativity *)
 
 fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute}
 
 
-
 (* definitional axioms *)
 
 fun def_axiom_disj ctxt t =
@@ -592,20 +567,17 @@
   ("disj", def_axiom_disj ctxt)] []
 
 
-
 (* application of definitions *)
 
 fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *)
   | apply_def ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Apply_Def thms t
 
 
-
 (* iff-oeq *)
 
 fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *)
 
 
-
 (* negation normal form *)
 
 fun nnf_prop ctxt thms t =
@@ -621,7 +593,6 @@
 fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg
 
 
-
 (* theory lemmas *)
 
 fun arith_th_lemma_tac ctxt prems =
@@ -642,7 +613,6 @@
   | NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms)
 
 
-
 (* mapping of rules to methods *)
 
 fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
@@ -693,4 +663,4 @@
 
 fun method_for rule = with_tracing rule (choose rule)
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_replay_rules.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -7,7 +7,7 @@
 signature Z3_NEW_REPLAY_RULES =
 sig
   val apply: Proof.context -> cterm -> thm option
-end
+end;
 
 structure Z3_New_Replay_Rules: Z3_NEW_REPLAY_RULES =
 struct
@@ -51,4 +51,4 @@
 val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
   Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Tools/SMT2/z3_new_replay_util.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -23,13 +23,11 @@
   (*simpset*)
   val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
   val make_simpset: Proof.context -> thm list -> simpset
-end
+end;
 
 structure Z3_New_Replay_Util: Z3_NEW_REPLAY_UTIL =
 struct
 
-
-
 (* theorem nets *)
 
 fun thm_net_of f xthms =
@@ -59,7 +57,6 @@
 end
 
 
-
 (* proof combinators *)
 
 fun under_assumption f ct =
@@ -68,7 +65,6 @@
 fun discharge p pq = Thm.implies_elim pq p
 
 
-
 (* a faster COMP *)
 
 type compose_data = cterm list * (cterm -> cterm list) * thm
@@ -82,7 +78,6 @@
   discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
 
 
-
 (* simpset *)
 
 local
@@ -152,4 +147,4 @@
 
 end
 
-end
+end;
diff -r d52012eabf0d -r 489083abce44 src/HOL/Word/Tools/smt2_word.ML
--- a/src/HOL/Word/Tools/smt2_word.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Word/Tools/smt2_word.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -9,12 +9,11 @@
 
 open Word_Lib
 
+
 (* SMT-LIB logic *)
 
 fun smtlib_logic ts =
-  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
-  then SOME "QF_AUFBV"
-  else NONE
+  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE
 
 
 (* SMT-LIB builtins *)
@@ -141,4 +140,4 @@
   SMTLIB2_Interface.add_logic (20, smtlib_logic) #>
   setup_builtins))
 
-end
+end;