reformat comments
authornoschinl
Mon Apr 13 11:58:18 2015 +0200 (2015-04-13)
changeset 60049e4a5dfee0f9c
parent 60048 e9c30726ca8e
child 60050 dc6ac152d864
reformat comments
src/HOL/Library/cconv.ML
     1.1 --- a/src/HOL/Library/cconv.ML	Mon Apr 13 10:39:49 2015 +0200
     1.2 +++ b/src/HOL/Library/cconv.ML	Mon Apr 13 11:58:18 2015 +0200
     1.3 @@ -126,9 +126,9 @@
     1.4           fun abstract_rule u v eq =
     1.5             let
     1.6               (* Take a variable v and an equality theorem of form:
     1.7 -                  P1 Pure.imp ... Pure.imp Pn Pure.imp L v == R v
     1.8 +                  P1 \<Longrightarrow> ... \<Longrightarrow> Pn \<Longrightarrow> L v \<equiv> R v
     1.9                  And build a term of form:
    1.10 -                  !!v. (%x. L x) v == (%x. R x) v *)
    1.11 +                  \<And>v. (\<lambda>x. L x) v \<equiv> (\<lambda>x. R x) v *)
    1.12               fun mk_concl var eq =
    1.13                 let
    1.14                   val certify = Thm.cterm_of ctxt
    1.15 @@ -165,7 +165,7 @@
    1.16  
    1.17  (* conversions on HHF rules *)
    1.18  
    1.19 -(*rewrite B in !!x1 ... xn. B*)
    1.20 +(*rewrite B in \<And>x1 ... xn. B*)
    1.21  fun params_cconv n cv ctxt ct =
    1.22    if n <> 0 andalso Logic.is_all (Thm.term_of ct)
    1.23    then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
    1.24 @@ -173,7 +173,7 @@
    1.25  
    1.26  (* TODO: This code behaves not exactly like Conv.prems_cconv does.
    1.27           Fix this! *)
    1.28 -(*rewrite the A's in A1 Pure.imp ... Pure.imp An Pure.imp B*)
    1.29 +(*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
    1.30  fun prems_cconv 0 cv ct = cv ct
    1.31    | prems_cconv n cv ct =
    1.32        (case ct |> Thm.term_of of
    1.33 @@ -181,7 +181,7 @@
    1.34            ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
    1.35        | _ =>  cv ct)
    1.36  
    1.37 -(*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
    1.38 +(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
    1.39  fun concl_cconv 0 cv ct = cv ct
    1.40    | concl_cconv n cv ct =
    1.41        (case ct |> Thm.term_of of