src/HOL/SMT.thy
changeset 60201 90e88e521e0e
parent 59960 372ddff01244
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/SMT.thy	Fri Apr 24 23:05:33 2015 +0200
     1.2 +++ b/src/HOL/SMT.thy	Sat Apr 25 09:48:06 2015 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  *}
     1.5  
     1.6  method_setup moura = {*
     1.7 - Scan.succeed (SIMPLE_METHOD' o moura_tac)
     1.8 +  Scan.succeed (SIMPLE_METHOD' o moura_tac)
     1.9  *} "solve skolemization goals, especially those arising from Z3 proofs"
    1.10  
    1.11  hide_fact (open) choices bchoices