# HG changeset patch
# User noschinl
# Date 1428919098 -7200
# Node ID e4a5dfee0f9c77183e340c57f6fddddd76078f81
# Parent  e9c30726ca8eacf2101450a6f9953f4e76baac34
reformat comments

diff -r e9c30726ca8e -r e4a5dfee0f9c src/HOL/Library/cconv.ML
--- a/src/HOL/Library/cconv.ML	Mon Apr 13 10:39:49 2015 +0200
+++ b/src/HOL/Library/cconv.ML	Mon Apr 13 11:58:18 2015 +0200
@@ -126,9 +126,9 @@
          fun abstract_rule u v eq =
            let
              (* Take a variable v and an equality theorem of form:
-                  P1 Pure.imp ... Pure.imp Pn Pure.imp L v == R v
+                  P1 \<Longrightarrow> ... \<Longrightarrow> Pn \<Longrightarrow> L v \<equiv> R v
                 And build a term of form:
-                  !!v. (%x. L x) v == (%x. R x) v *)
+                  \<And>v. (\<lambda>x. L x) v \<equiv> (\<lambda>x. R x) v *)
              fun mk_concl var eq =
                let
                  val certify = Thm.cterm_of ctxt
@@ -165,7 +165,7 @@
 
 (* conversions on HHF rules *)
 
-(*rewrite B in !!x1 ... xn. B*)
+(*rewrite B in \<And>x1 ... xn. B*)
 fun params_cconv n cv ctxt ct =
   if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
@@ -173,7 +173,7 @@
 
 (* TODO: This code behaves not exactly like Conv.prems_cconv does.
          Fix this! *)
-(*rewrite the A's in A1 Pure.imp ... Pure.imp An Pure.imp B*)
+(*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
 fun prems_cconv 0 cv ct = cv ct
   | prems_cconv n cv ct =
       (case ct |> Thm.term_of of
@@ -181,7 +181,7 @@
           ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
       | _ =>  cv ct)
 
-(*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
+(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
 fun concl_cconv 0 cv ct = cv ct
   | concl_cconv n cv ct =
       (case ct |> Thm.term_of of