code indentation
authorblanchet
Wed Sep 05 19:57:50 2012 +0200 (2012-09-05)
changeset 49168766a09b84562
parent 49167 68623861e0f2
child 49169 937a0fadddfb
code indentation
src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 16:17:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 19:57:50 2012 +0200
     1.3 @@ -97,8 +97,6 @@
     1.4  val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
     1.5  
     1.6  fun mk_split_asm_tac ctxt split =
     1.7 -  rtac (split RS trans) 1 THEN
     1.8 -  Local_Defs.unfold_tac ctxt split_asm_thms THEN
     1.9 -  rtac refl 1;
    1.10 +  rtac (split RS trans) 1 THEN Local_Defs.unfold_tac ctxt split_asm_thms THEN rtac refl 1;
    1.11  
    1.12  end;