# HG changeset patch
# User wenzelm
# Date 1516093086 -3600
# Node ID 100247708f314de8544582a265cb2c516ab34432
# Parent  3abf6a7225181076b9a462eb7d345892e8e158d8
clarified comments;

diff -r 3abf6a722518 -r 100247708f31 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Tue Jan 16 09:30:00 2018 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Tue Jan 16 09:58:06 2018 +0100
@@ -24,20 +24,15 @@
   {List tl q (rev Ps @ Qs)}"
 apply vcg_simp
   apply fastforce
- apply(fastforce intro:notin_List_update[THEN iffD2])
-(* explicit:
- apply clarify
- apply(rename_tac ps b qs)
- apply clarsimp
- apply(rename_tac ps')
- apply(fastforce intro:notin_List_update[THEN iffD2])
- apply(rule_tac x = ps' in exI)
- apply simp
- apply(rule_tac x = "b#qs" in exI)
- apply simp
-*)
-apply fastforce
-done
+  apply(fastforce intro:notin_List_update[THEN iffD2])
+  \<comment> \<open>explicit:\<close>
+  \<^cancel>\<open>apply clarify\<close>
+  \<^cancel>\<open>apply(rename_tac ps b qs)\<close>
+  \<^cancel>\<open>apply clarsimp\<close>
+  \<^cancel>\<open>apply(rename_tac ps')\<close>
+  \<^cancel>\<open>apply(fastforce intro:notin_List_update[THEN iffD2])\<close>
+  apply fastforce
+  done
 
 text\<open>And now with ghost variables @{term ps} and @{term qs}. Even
 ``more automatic''.\<close>
diff -r 3abf6a722518 -r 100247708f31 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Tue Jan 16 09:30:00 2018 +0100
+++ b/src/HOL/Hoare/Pointers0.thy	Tue Jan 16 09:58:06 2018 +0100
@@ -188,19 +188,18 @@
   {List tl q (rev Ps @ Qs)}"
 apply vcg_simp
   apply fastforce
- apply(fastforce intro:notin_List_update[THEN iffD2])
-(* explicily:
- apply clarify
- apply(rename_tac ps qs)
- apply clarsimp
- apply(rename_tac ps')
- apply(rule_tac x = ps' in exI)
- apply simp
- apply(rule_tac x = "p#qs" in exI)
- apply simp
-*)
-apply fastforce
-done
+  apply(fastforce intro:notin_List_update[THEN iffD2])
+  \<comment> \<open>explicit:\<close>
+  \<^cancel>\<open>apply clarify\<close>
+  \<^cancel>\<open>apply(rename_tac ps qs)\<close>
+  \<^cancel>\<open>apply clarsimp\<close>
+  \<^cancel>\<open>apply(rename_tac ps')\<close>
+  \<^cancel>\<open>apply(rule_tac x = ps' in exI)\<close>
+  \<^cancel>\<open>apply simp\<close>
+  \<^cancel>\<open>apply(rule_tac x = "p#qs" in exI)\<close>
+  \<^cancel>\<open>apply simp\<close>
+  apply fastforce
+  done
 
 
 text "A longer readable version:"
diff -r 3abf6a722518 -r 100247708f31 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Tue Jan 16 09:30:00 2018 +0100
+++ b/src/HOL/Hoare/Separation.thy	Tue Jan 16 09:58:06 2018 +0100
@@ -54,13 +54,11 @@
  "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
 
 (* FIXME does not handle "_idtdummy" *)
-ML\<open>
-(* free_tr takes care of free vars in the scope of sep. logic connectives:
-   they are implicitly applied to the heap *)
+ML \<open>
+\<comment> \<open>\<open>free_tr\<close> takes care of free vars in the scope of separation logic connectives:
+    they are implicitly applied to the heap\<close>
 fun free_tr(t as Free _) = t $ Syntax.free "H"
-(*
-  | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps
-*)
+\<^cancel>\<open>| free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps\<close>
   | free_tr t = t
 
 fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H"
@@ -109,9 +107,7 @@
 
 fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
   | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
-(*
-  | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps
-*)
+\<^cancel>\<open>| strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps\<close>
   | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   | strip (Abs(_,_,P)) = P
   | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}