# HG changeset patch
# User nipkow
# Date 1389092749 -3600
# Node ID 6d99745afe34028ed7a3fba768bfa54dd9bc6a88
# Parent  a20b105bb5d1b3783a7094ae42569946c9aefdcc
tuned

diff -r a20b105bb5d1 -r 6d99745afe34 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Mon Jan 06 23:00:11 2014 +0100
+++ b/src/HOL/IMP/ACom.thy	Tue Jan 07 12:05:49 2014 +0100
@@ -15,9 +15,11 @@
   While 'a bexp 'a "('a acom)" 'a
     ("({_}//WHILE _//DO ({_}//_)//{_})"  [0, 0, 0, 61, 0] 61)
 
+notation com.SKIP ("SKIP")
+
 text_raw{*\snip{stripdef}{1}{1}{% *}
 fun strip :: "'a acom \<Rightarrow> com" where
-"strip (SKIP {P}) = com.SKIP" |
+"strip (SKIP {P}) = SKIP" |
 "strip (x ::= e {P}) = x ::= e" |
 "strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" |
 "strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) =
@@ -27,7 +29,7 @@
 
 text_raw{*\snip{asizedef}{1}{1}{% *}
 fun asize :: "com \<Rightarrow> nat" where
-"asize com.SKIP = 1" |
+"asize SKIP = 1" |
 "asize (x ::= e) = 1" |
 "asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" |
 "asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" |
@@ -39,7 +41,7 @@
 "shift f n = (\<lambda>p. f(p+n))"
 
 fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
-"annotate f com.SKIP = SKIP {f 0}" |
+"annotate f SKIP = SKIP {f 0}" |
 "annotate f (x ::= e) = x ::= e {f 0}" |
 "annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" |
 "annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
@@ -131,7 +133,7 @@
 done
 
 lemma strip_eq_SKIP:
-  "strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})"
+  "strip C = SKIP \<longleftrightarrow> (EX P. C = SKIP {P})"
 by (cases C) simp_all
 
 lemma strip_eq_Assign:
diff -r a20b105bb5d1 -r 6d99745afe34 src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Mon Jan 06 23:00:11 2014 +0100
+++ b/src/HOL/IMP/VCG.thy	Tue Jan 07 12:05:49 2014 +0100
@@ -14,11 +14,12 @@
   Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
   Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
 
+notation com.SKIP ("SKIP")
 
 text{* Strip annotations: *}
 
 fun strip :: "acom \<Rightarrow> com" where
-"strip SKIP = com.SKIP" |
+"strip SKIP = SKIP" |
 "strip (x ::= a) = (x ::= a)" |
 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" |
 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |