# HG changeset patch
# User wenzelm
# Date 1515359754 -3600
# Node ID 7360fe6bb423acd25202e38745d10aaa47e48db1
# Parent  e9bee1ddfe19c1cd5652b25fc35ee4cf72b7f17f
prefer formal comments;

diff -r e9bee1ddfe19 -r 7360fe6bb423 src/Doc/Isar_Ref/Synopsis.thy
--- a/src/Doc/Isar_Ref/Synopsis.thy	Sun Jan 07 21:32:21 2018 +0100
+++ b/src/Doc/Isar_Ref/Synopsis.thy	Sun Jan 07 22:15:54 2018 +0100
@@ -952,10 +952,10 @@
 notepad
 begin
   assume r:
-    "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  (* assumptions *)
-      (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 1 *)
-      (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 2 *)
-      R  (* main conclusion *)"
+    "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  \<comment> \<open>assumptions\<close>
+      (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  \<comment> \<open>case 1\<close>
+      (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  \<comment> \<open>case 2\<close>
+      R  \<comment> \<open>main conclusion\<close>"
 
   have A\<^sub>1 and A\<^sub>2 \<proof>
   then have R
diff -r e9bee1ddfe19 -r 7360fe6bb423 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Jan 07 22:15:54 2018 +0100
@@ -2893,7 +2893,7 @@
   where
     "divide_poly_main lc q r d dr (Suc n) =
       (let cr = coeff r dr; a = cr div lc; mon = monom a n in
-        if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
+        if False \<or> a * lc = cr then \<comment> \<open>\<open>False \<or>\<close> is only because of problem in function-package\<close>
           divide_poly_main
             lc
             (q + mon)
diff -r e9bee1ddfe19 -r 7360fe6bb423 src/HOL/Data_Structures/AA_Set.thy
--- a/src/HOL/Data_Structures/AA_Set.thy	Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy	Sun Jan 07 22:15:54 2018 +0100
@@ -29,7 +29,7 @@
 
 fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
 "split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
-   (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
+   (if lva = lvb \<and> lvb = lvc \<comment> \<open>\<open>lva = lvc\<close> suffices\<close>
     then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
     else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
 "split t = t"
diff -r e9bee1ddfe19 -r 7360fe6bb423 src/HOL/HOLCF/IOA/ABP/Spec.thy
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Jan 07 22:15:54 2018 +0100
@@ -22,7 +22,7 @@
         in
         case fst(snd(tr))
         of
-        Next =>  t=s |            (* Note that there is condition as in Sender *)
+        Next =>  t=s |           \<comment> \<open>Note that there is condition as in Sender\<close>
         S_msg(m) => t = s@[m]  |
         R_msg(m) => s = (m#t)  |
         S_pkt(pkt) => False |
diff -r e9bee1ddfe19 -r 7360fe6bb423 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Jan 07 22:15:54 2018 +0100
@@ -44,7 +44,7 @@
 "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
  s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
    roomk := (roomk s)(r := k'),
-   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
+   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<comment> \<open>\<open>\<and> k' = currk s r\<close>\<close>
                          \<or> safe s r)\<rparr> \<in> reach" |
 exit_room:
 "\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
diff -r e9bee1ddfe19 -r 7360fe6bb423 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 07 22:15:54 2018 +0100
@@ -725,7 +725,7 @@
           Some x \<Rightarrow> Some x
       | None \<Rightarrow> full_exhaustive_class.full_exhaustive
           (\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
-          (min (i - 1) 8) (* generate at most 8 bits *)
+          (min (i - 1) 8) \<comment> \<open>generate at most 8 bits\<close>
       else None)"
 
 instance ..