--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sat Jan 13 11:22:46 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Sat Jan 13 11:42:30 2018 +0100
@@ -442,7 +442,7 @@
primrec insort\<^sub>1 where
"insort\<^sub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
"insort\<^sub>1 (N y k t u) x =
- (* (split \<circ> skew) *) (N y k (if x < y then insort\<^sub>1 t x else t)
+ \<^cancel>\<open>(split \<circ> skew)\<close> (N y k (if x < y then insort\<^sub>1 t x else t)
(if x > y then insort\<^sub>1 u x else u))"
theorem wf_insort\<^sub>1: "wf t \<Longrightarrow> wf (insort\<^sub>1 t x)"
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Sat Jan 13 11:22:46 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Sat Jan 13 11:42:30 2018 +0100
@@ -52,7 +52,7 @@
"roomk [] r = initk r"
| "roomk (e#s) r = (let k = roomk s r in
case e of Check_in g r' c \<Rightarrow> k
- | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
+ | Enter g r' (x,y) \<Rightarrow> if r' = r \<^cancel>\<open>\<and> x = k\<close> then y else k
| Exit g r \<Rightarrow> k)"
primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Sat Jan 13 11:22:46 2018 +0100
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Sat Jan 13 11:42:30 2018 +0100
@@ -54,7 +54,7 @@
"roomk [] r = initk r"
| "roomk (e#s) r = (let k = roomk s r in
case e of Check_in g r' c \<Rightarrow> k
- | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
+ | Enter g r' (x,y) \<Rightarrow> if r' = r \<^cancel>\<open>\<and> x = k\<close> then y else k
| Exit g r \<Rightarrow> k)"
primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy Sat Jan 13 11:22:46 2018 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy Sat Jan 13 11:42:30 2018 +0100
@@ -177,7 +177,7 @@
fun l_bal where
"l_bal(n, MKT ln ll lr h, r) =
(if ht ll < ht lr
- then case lr of ET \<Rightarrow> ET (* impossible *)
+ then case lr of ET \<Rightarrow> ET \<comment> \<open>impossible\<close>
| MKT lrn lrr lrl lrh \<Rightarrow>
mkt lrn (mkt ln ll lrl) (mkt n lrr r)
else mkt ln ll (mkt n lr r))"
@@ -185,7 +185,7 @@
fun r_bal where
"r_bal(n, l, MKT rn rl rr h) =
(if ht rl > ht rr
- then case rl of ET \<Rightarrow> ET (* impossible *)
+ then case rl of ET \<Rightarrow> ET \<comment> \<open>impossible\<close>
| MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr)
else mkt rn (mkt n l rl) rr)"