--- 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
--- 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)
--- 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"
--- 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 |
--- 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"
--- 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 ..