src/HOL/Library/cconv.ML
changeset 59975 da10875adf8e
parent 59739 4ed50ebf5d36
child 60048 e9c30726ca8e
     1.1 --- a/src/HOL/Library/cconv.ML	Wed Apr 08 21:08:26 2015 +0200
     1.2 +++ b/src/HOL/Library/cconv.ML	Wed Apr 08 21:24:27 2015 +0200
     1.3 @@ -1,3 +1,9 @@
     1.4 +(*  Title:      HOL/Library/cconv.ML
     1.5 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     1.6 +
     1.7 +FIXME!?
     1.8 +*)
     1.9 +
    1.10  infix 1 then_cconv
    1.11  infix 0 else_cconv
    1.12  
    1.13 @@ -170,7 +176,8 @@
    1.14  fun prems_cconv 0 cv ct = cv ct
    1.15    | prems_cconv n cv ct =
    1.16        (case ct |> Thm.term_of of
    1.17 -        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
    1.18 +        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
    1.19 +          ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
    1.20        | _ =>  cv ct)
    1.21  
    1.22  (*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
    1.23 @@ -212,7 +219,7 @@
    1.24        end
    1.25    | NONE => raise THM ("gconv_rule", i, [th]))
    1.26  
    1.27 -  (* Conditional conversions as tactics. *)
    1.28 +(* Conditional conversions as tactics. *)
    1.29  fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
    1.30    handle THM _ => Seq.empty
    1.31         | CTERM _ => Seq.empty