replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
authornipkow
Fri May 17 08:19:52 2013 +0200 (2013-05-17)
changeset 52046bc01725d7918
parent 52045 90cd3c53a887
child 52047 0476162187c4
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
src/HOL/IMP/ACom.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
src/HOL/IMP/Abs_Int_Tests.thy
src/HOL/IMP/Big_Step.thy
src/HOL/IMP/Collecting.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Def_Init.thy
src/HOL/IMP/Def_Init_Big.thy
src/HOL/IMP/Def_Init_Small.thy
src/HOL/IMP/Def_Init_Sound_Small.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Finite_Reachable.thy
src/HOL/IMP/Fold.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/HoareT.thy
src/HOL/IMP/Hoare_Examples.thy
src/HOL/IMP/Hoare_Sound_Complete.thy
src/HOL/IMP/Live.thy
src/HOL/IMP/Live_True.thy
src/HOL/IMP/Poly_Types.thy
src/HOL/IMP/Procs.thy
src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Stat.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
src/HOL/IMP/Sem_Equiv.thy
src/HOL/IMP/Small_Step.thy
src/HOL/IMP/Types.thy
src/HOL/IMP/VC.thy
src/HOL/IMP/Vars.thy
     1.1 --- a/src/HOL/IMP/ACom.thy	Fri May 17 02:57:00 2013 +0200
     1.2 +++ b/src/HOL/IMP/ACom.thy	Fri May 17 08:19:52 2013 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  datatype 'a acom =
     1.5    SKIP 'a                           ("SKIP {_}" 61) |
     1.6    Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
     1.7 -  Seq "('a acom)" "('a acom)"       ("_;//_"  [60, 61] 60) |
     1.8 +  Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
     1.9    If bexp 'a "('a acom)" 'a "('a acom)" 'a
    1.10      ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})"  [0, 0, 0, 61, 0, 0] 61) |
    1.11    While 'a bexp 'a "('a acom)" 'a
    1.12 @@ -19,7 +19,7 @@
    1.13  fun strip :: "'a acom \<Rightarrow> com" where
    1.14  "strip (SKIP {P}) = com.SKIP" |
    1.15  "strip (x ::= e {P}) = x ::= e" |
    1.16 -"strip (C\<^isub>1;C\<^isub>2) = strip C\<^isub>1; strip C\<^isub>2" |
    1.17 +"strip (C\<^isub>1;;C\<^isub>2) = strip C\<^isub>1;; strip C\<^isub>2" |
    1.18  "strip (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {P}) =
    1.19    IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2" |
    1.20  "strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
    1.21 @@ -29,7 +29,7 @@
    1.22  fun asize :: "com \<Rightarrow> nat" where
    1.23  "asize com.SKIP = 1" |
    1.24  "asize (x ::= e) = 1" |
    1.25 -"asize (C\<^isub>1;C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2" |
    1.26 +"asize (C\<^isub>1;;C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2" |
    1.27  "asize (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2 + 3" |
    1.28  "asize (WHILE b DO C) = asize C + 3"
    1.29  text_raw{*}%endsnip*}
    1.30 @@ -41,7 +41,7 @@
    1.31  fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
    1.32  "annotate f com.SKIP = SKIP {f 0}" |
    1.33  "annotate f (x ::= e) = x ::= e {f 0}" |
    1.34 -"annotate f (c\<^isub>1;c\<^isub>2) = annotate f c\<^isub>1; annotate (shift f (asize c\<^isub>1)) c\<^isub>2" |
    1.35 +"annotate f (c\<^isub>1;;c\<^isub>2) = annotate f c\<^isub>1;; annotate (shift f (asize c\<^isub>1)) c\<^isub>2" |
    1.36  "annotate f (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
    1.37    IF b THEN {f 0} annotate (shift f 1) c\<^isub>1
    1.38    ELSE {f(asize c\<^isub>1 + 1)} annotate (shift f (asize c\<^isub>1 + 2)) c\<^isub>2
    1.39 @@ -54,7 +54,7 @@
    1.40  fun annos :: "'a acom \<Rightarrow> 'a list" where
    1.41  "annos (SKIP {P}) = [P]" |
    1.42  "annos (x ::= e {P}) = [P]" |
    1.43 -"annos (C\<^isub>1;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" |
    1.44 +"annos (C\<^isub>1;;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" |
    1.45  "annos (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
    1.46    P\<^isub>1 # annos C\<^isub>1 @  P\<^isub>2 # annos C\<^isub>2 @ [Q]" |
    1.47  "annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
    1.48 @@ -70,7 +70,7 @@
    1.49  fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
    1.50  "map_acom f (SKIP {P}) = SKIP {f P}" |
    1.51  "map_acom f (x ::= e {P}) = x ::= e {f P}" |
    1.52 -"map_acom f (C\<^isub>1;C\<^isub>2) = map_acom f C\<^isub>1; map_acom f C\<^isub>2" |
    1.53 +"map_acom f (C\<^isub>1;;C\<^isub>2) = map_acom f C\<^isub>1;; map_acom f C\<^isub>2" |
    1.54  "map_acom f (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
    1.55    IF b THEN {f P\<^isub>1} map_acom f C\<^isub>1 ELSE {f P\<^isub>2} map_acom f C\<^isub>2
    1.56    {f Q}" |
    1.57 @@ -139,7 +139,7 @@
    1.58  by (cases C) simp_all
    1.59  
    1.60  lemma strip_eq_Seq:
    1.61 -  "strip C = c1;c2 \<longleftrightarrow> (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)"
    1.62 +  "strip C = c1;;c2 \<longleftrightarrow> (EX C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)"
    1.63  by (cases C) simp_all
    1.64  
    1.65  lemma strip_eq_If:
     2.1 --- a/src/HOL/IMP/Abs_Int0.thy	Fri May 17 02:57:00 2013 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Fri May 17 08:19:52 2013 +0200
     2.3 @@ -378,7 +378,7 @@
     2.4  lemma top_on_acom_simps:
     2.5    "top_on_acom (SKIP {Q}) X = top_on_opt Q X"
     2.6    "top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
     2.7 -  "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
     2.8 +  "top_on_acom (C1;;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
     2.9    "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
    2.10     (top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
    2.11    "top_on_acom ({I} WHILE b DO {P} C {Q}) X =
     3.1 --- a/src/HOL/IMP/Abs_Int1.thy	Fri May 17 02:57:00 2013 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Fri May 17 08:19:52 2013 +0200
     3.3 @@ -156,7 +156,7 @@
     3.4  lemma top_on_acom_simps:
     3.5    "top_on_acom (SKIP {Q}) X = top_on_opt Q X"
     3.6    "top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
     3.7 -  "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
     3.8 +  "top_on_acom (C1;;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
     3.9    "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
    3.10     (top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
    3.11    "top_on_acom ({I} WHILE b DO {P} C {Q}) X =
     4.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Fri May 17 02:57:00 2013 +0200
     4.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri May 17 08:19:52 2013 +0200
     4.3 @@ -133,12 +133,12 @@
     4.4  subsubsection "Tests"
     4.5  
     4.6  definition "test1_parity =
     4.7 -  ''x'' ::= N 1;
     4.8 +  ''x'' ::= N 1;;
     4.9    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
    4.10  value [code] "show_acom (the(AI_parity test1_parity))"
    4.11  
    4.12  definition "test2_parity =
    4.13 -  ''x'' ::= N 1;
    4.14 +  ''x'' ::= N 1;;
    4.15    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
    4.16  
    4.17  definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"
     5.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Fri May 17 02:57:00 2013 +0200
     5.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Fri May 17 08:19:52 2013 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4  fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
     5.5  "AI SKIP S = S" |
     5.6  "AI (x ::= a) S = update S x (aval' a S)" |
     5.7 -"AI (c1;c2) S = AI c2 (AI c1 S)" |
     5.8 +"AI (c1;;c2) S = AI c2 (AI c1 S)" |
     5.9  "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
    5.10  "AI (WHILE b DO c) S = pfp (AI c) S"
    5.11  
     6.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Fri May 17 02:57:00 2013 +0200
     6.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Fri May 17 08:19:52 2013 +0200
     6.3 @@ -68,8 +68,8 @@
     6.4  
     6.5  text{* Straight line code: *}
     6.6  definition "test1_const =
     6.7 - ''y'' ::= N 7;
     6.8 - ''z'' ::= Plus (V ''y'') (N 2);
     6.9 + ''y'' ::= N 7;;
    6.10 + ''z'' ::= Plus (V ''y'') (N 2);;
    6.11   ''y'' ::= Plus (V ''x'') (N 0)"
    6.12  
    6.13  text{* Conditional: *}
    6.14 @@ -78,27 +78,27 @@
    6.15  
    6.16  text{* Conditional, test is ignored: *}
    6.17  definition "test3_const =
    6.18 - ''x'' ::= N 42;
    6.19 + ''x'' ::= N 42;;
    6.20   IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
    6.21  
    6.22  text{* While: *}
    6.23  definition "test4_const =
    6.24 - ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
    6.25 + ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
    6.26  
    6.27  text{* While, test is ignored: *}
    6.28  definition "test5_const =
    6.29 - ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
    6.30 + ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
    6.31  
    6.32  text{* Iteration is needed: *}
    6.33  definition "test6_const =
    6.34 -  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
    6.35 -  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
    6.36 +  ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
    6.37 +  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
    6.38  
    6.39  text{* More iteration would be needed: *}
    6.40  definition "test7_const =
    6.41 -  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
    6.42 +  ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 0;; ''u'' ::= N 3;;
    6.43    WHILE Less (V ''x'') (N 1)
    6.44 -  DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
    6.45 +  DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')"
    6.46  
    6.47  value [code] "list (AI_const test1_const Top)"
    6.48  value [code] "list (AI_const test2_const Top)"
     7.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Fri May 17 02:57:00 2013 +0200
     7.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Fri May 17 08:19:52 2013 +0200
     7.3 @@ -150,7 +150,7 @@
     7.4  fun AI :: "com \<Rightarrow> 'a st \<Rightarrow> 'a st" where
     7.5  "AI SKIP S = S" |
     7.6  "AI (x ::= a) S = S(x := aval' a S)" |
     7.7 -"AI (c1;c2) S = AI c2 (AI c1 S)" |
     7.8 +"AI (c1;;c2) S = AI c2 (AI c1 S)" |
     7.9  "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
    7.10  "AI (WHILE b DO c) S = pfp (AI c) S"
    7.11  
     8.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Fri May 17 02:57:00 2013 +0200
     8.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Fri May 17 08:19:52 2013 +0200
     8.3 @@ -174,7 +174,7 @@
     8.4  "AI SKIP S = S" |
     8.5  "AI (x ::= a) S =
     8.6    (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
     8.7 -"AI (c1;c2) S = AI c2 (AI c1 S)" |
     8.8 +"AI (c1;;c2) S = AI c2 (AI c1 S)" |
     8.9  "AI (IF b THEN c1 ELSE c2) S =
    8.10    AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
    8.11  "AI (WHILE b DO c) S =
     9.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Fri May 17 02:57:00 2013 +0200
     9.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Fri May 17 08:19:52 2013 +0200
     9.3 @@ -232,7 +232,7 @@
     9.4    (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
     9.5  
     9.6  definition "test_ivl1 =
     9.7 - ''y'' ::= N 7;
     9.8 + ''y'' ::= N 7;;
     9.9   IF Less (V ''x'') (V ''y'')
    9.10   THEN ''y'' ::= Plus (V ''y'') (V ''x'')
    9.11   ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
    9.12 @@ -245,25 +245,25 @@
    9.13  value "list_up (AI_ivl test6_const Top)"
    9.14  
    9.15  definition "test2_ivl =
    9.16 - ''y'' ::= N 7;
    9.17 + ''y'' ::= N 7;;
    9.18   WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
    9.19  value [code] "list_up(AI_ivl test2_ivl Top)"
    9.20  
    9.21  definition "test3_ivl =
    9.22 - ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
    9.23 + ''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
    9.24   WHILE Less (V ''x'') (N 11)
    9.25 - DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
    9.26 + DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
    9.27  value [code] "list_up(AI_ivl test3_ivl Top)"
    9.28  
    9.29  definition "test4_ivl =
    9.30 - ''x'' ::= N 0; ''y'' ::= N 0;
    9.31 + ''x'' ::= N 0;; ''y'' ::= N 0;;
    9.32   WHILE Less (V ''x'') (N 1001)
    9.33 - DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
    9.34 + DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
    9.35  value [code] "list_up(AI_ivl test4_ivl Top)"
    9.36  
    9.37  text{* Nontermination not detected: *}
    9.38  definition "test5_ivl =
    9.39 - ''x'' ::= N 0;
    9.40 + ''x'' ::= N 0;;
    9.41   WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
    9.42  value [code] "list_up(AI_ivl test5_ivl Top)"
    9.43  
    10.1 --- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Fri May 17 02:57:00 2013 +0200
    10.2 +++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Fri May 17 08:19:52 2013 +0200
    10.3 @@ -9,7 +9,7 @@
    10.4  datatype 'a acom =
    10.5    SKIP 'a                           ("SKIP {_}" 61) |
    10.6    Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
    10.7 -  Seq "('a acom)" "('a acom)"       ("_;//_"  [60, 61] 60) |
    10.8 +  Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
    10.9    If bexp "('a acom)" "('a acom)" 'a
   10.10      ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
   10.11    While 'a bexp "('a acom)" 'a
   10.12 @@ -18,21 +18,21 @@
   10.13  fun post :: "'a acom \<Rightarrow>'a" where
   10.14  "post (SKIP {P}) = P" |
   10.15  "post (x ::= e {P}) = P" |
   10.16 -"post (c1; c2) = post c2" |
   10.17 +"post (c1;; c2) = post c2" |
   10.18  "post (IF b THEN c1 ELSE c2 {P}) = P" |
   10.19  "post ({Inv} WHILE b DO c {P}) = P"
   10.20  
   10.21  fun strip :: "'a acom \<Rightarrow> com" where
   10.22  "strip (SKIP {P}) = com.SKIP" |
   10.23  "strip (x ::= e {P}) = (x ::= e)" |
   10.24 -"strip (c1;c2) = (strip c1; strip c2)" |
   10.25 +"strip (c1;;c2) = (strip c1;; strip c2)" |
   10.26  "strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
   10.27  "strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)"
   10.28  
   10.29  fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
   10.30  "anno a com.SKIP = SKIP {a}" |
   10.31  "anno a (x ::= e) = (x ::= e {a})" |
   10.32 -"anno a (c1;c2) = (anno a c1; anno a c2)" |
   10.33 +"anno a (c1;;c2) = (anno a c1;; anno a c2)" |
   10.34  "anno a (IF b THEN c1 ELSE c2) =
   10.35    (IF b THEN anno a c1 ELSE anno a c2 {a})" |
   10.36  "anno a (WHILE b DO c) =
   10.37 @@ -41,14 +41,14 @@
   10.38  fun annos :: "'a acom \<Rightarrow> 'a list" where
   10.39  "annos (SKIP {a}) = [a]" |
   10.40  "annos (x::=e {a}) = [a]" |
   10.41 -"annos (C1;C2) = annos C1 @ annos C2" |
   10.42 +"annos (C1;;C2) = annos C1 @ annos C2" |
   10.43  "annos (IF b THEN C1 ELSE C2 {a}) = a #  annos C1 @ annos C2" |
   10.44  "annos ({i} WHILE b DO C {a}) = i # a # annos C"
   10.45  
   10.46  fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
   10.47  "map_acom f (SKIP {P}) = SKIP {f P}" |
   10.48  "map_acom f (x ::= e {P}) = (x ::= e {f P})" |
   10.49 -"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
   10.50 +"map_acom f (c1;;c2) = (map_acom f c1;; map_acom f c2)" |
   10.51  "map_acom f (IF b THEN c1 ELSE c2 {P}) =
   10.52    (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" |
   10.53  "map_acom f ({Inv} WHILE b DO c {P}) =
   10.54 @@ -70,8 +70,8 @@
   10.55  by (cases c) auto
   10.56  
   10.57  lemma map_acom_Seq:
   10.58 - "map_acom f c = c1';c2' \<longleftrightarrow>
   10.59 - (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
   10.60 + "map_acom f c = c1';;c2' \<longleftrightarrow>
   10.61 + (\<exists>c1 c2. c = c1;;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
   10.62  by (cases c) auto
   10.63  
   10.64  lemma map_acom_If:
   10.65 @@ -97,7 +97,7 @@
   10.66  by (cases c) simp_all
   10.67  
   10.68  lemma strip_eq_Seq:
   10.69 -  "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
   10.70 +  "strip c = c1;;c2 \<longleftrightarrow> (EX d1 d2. c = d1;;d2 & strip d1 = c1 & strip d2 = c2)"
   10.71  by (cases c) simp_all
   10.72  
   10.73  lemma strip_eq_If:
    11.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Fri May 17 02:57:00 2013 +0200
    11.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Fri May 17 08:19:52 2013 +0200
    11.3 @@ -72,7 +72,7 @@
    11.4  fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
    11.5  "le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
    11.6  "le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
    11.7 -"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
    11.8 +"le_acom (c1;;c2) (c1';;c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
    11.9  "le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
   11.10    (b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" |
   11.11  "le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
   11.12 @@ -85,7 +85,7 @@
   11.13  lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')"
   11.14  by (cases c) auto
   11.15  
   11.16 -lemma [simp]: "c1;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
   11.17 +lemma [simp]: "c1;;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';;c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
   11.18  by (cases c) auto
   11.19  
   11.20  lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow>
   11.21 @@ -263,7 +263,7 @@
   11.22  "step' S (SKIP {P}) = (SKIP {S})" |
   11.23  "step' S (x ::= e {P}) =
   11.24    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
   11.25 -"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
   11.26 +"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" |
   11.27  "step' S (IF b THEN c1 ELSE c2 {P}) =
   11.28     IF b THEN step' S c1 ELSE step' S c2 {post c1 \<squnion> post c2}" |
   11.29  "step' S ({Inv} WHILE b DO c {P}) =
    12.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Fri May 17 02:57:00 2013 +0200
    12.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Fri May 17 08:19:52 2013 +0200
    12.3 @@ -33,7 +33,7 @@
    12.4  "step' S (SKIP {P}) = (SKIP {S})" |
    12.5  "step' S (x ::= e {P}) =
    12.6    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
    12.7 -"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
    12.8 +"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" |
    12.9  "step' S (IF b THEN c1 ELSE c2 {P}) =
   12.10    (let c1' = step' S c1; c2' = step' S c2
   12.11     in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
    13.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Fri May 17 02:57:00 2013 +0200
    13.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Fri May 17 08:19:52 2013 +0200
    13.3 @@ -122,13 +122,13 @@
    13.4  subsubsection "Tests"
    13.5  
    13.6  definition "test1_parity =
    13.7 -  ''x'' ::= N 1;
    13.8 +  ''x'' ::= N 1;;
    13.9    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
   13.10  
   13.11  value "show_acom_opt (AI_parity test1_parity)"
   13.12  
   13.13  definition "test2_parity =
   13.14 -  ''x'' ::= N 1;
   13.15 +  ''x'' ::= N 1;;
   13.16    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
   13.17  
   13.18  value "show_acom ((step_parity \<top> ^^1) (anno None test2_parity))"
    14.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Fri May 17 02:57:00 2013 +0200
    14.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Fri May 17 08:19:52 2013 +0200
    14.3 @@ -148,7 +148,7 @@
    14.4  "step' S (SKIP {P}) = (SKIP {S})" |
    14.5  "step' S (x ::= e {P}) =
    14.6    x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
    14.7 -"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
    14.8 +"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" |
    14.9  "step' S (IF b THEN c1 ELSE c2 {P}) =
   14.10    (let c1' = step' (bfilter b True S) c1; c2' = step' (bfilter b False S) c2
   14.11     in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
    15.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Fri May 17 02:57:00 2013 +0200
    15.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Fri May 17 08:19:52 2013 +0200
    15.3 @@ -107,7 +107,7 @@
    15.4  fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
    15.5  "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
    15.6  "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
    15.7 -"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
    15.8 +"map2_acom f (c1;;c2) (c1';;c2') = (map2_acom f c1 c1';; map2_acom f c2 c2')" |
    15.9  "map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
   15.10    (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
   15.11  "map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
    16.1 --- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Fri May 17 02:57:00 2013 +0200
    16.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Fri May 17 08:19:52 2013 +0200
    16.3 @@ -17,7 +17,7 @@
    16.4  fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
    16.5  "(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')" |
    16.6  "(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
    16.7 -"(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
    16.8 +"(c1;;c2) \<le> (c1';;c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
    16.9  "(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) =
   16.10    (b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" |
   16.11  "({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) =
   16.12 @@ -30,7 +30,7 @@
   16.13  lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
   16.14  by (cases c) auto
   16.15  
   16.16 -lemma Seq_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
   16.17 +lemma Seq_le: "c1;;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';;c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
   16.18  by (cases c) auto
   16.19  
   16.20  lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
   16.21 @@ -64,12 +64,12 @@
   16.22  end
   16.23  
   16.24  fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
   16.25 -"sub\<^isub>1(c1;c2) = c1" |
   16.26 +"sub\<^isub>1(c1;;c2) = c1" |
   16.27  "sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
   16.28  "sub\<^isub>1({I} WHILE b DO c {P}) = c"
   16.29  
   16.30  fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
   16.31 -"sub\<^isub>2(c1;c2) = c2" |
   16.32 +"sub\<^isub>2(c1;;c2) = c2" |
   16.33  "sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2"
   16.34  
   16.35  fun invar :: "'a acom \<Rightarrow> 'a" where
   16.36 @@ -79,8 +79,8 @@
   16.37  where
   16.38  "lift F com.SKIP M = (SKIP {F (post ` M)})" |
   16.39  "lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
   16.40 -"lift F (c1;c2) M =
   16.41 -  lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
   16.42 +"lift F (c1;;c2) M =
   16.43 +  lift F c1 (sub\<^isub>1 ` M);; lift F c2 (sub\<^isub>2 ` M)" |
   16.44  "lift F (IF b THEN c1 ELSE c2) M =
   16.45    IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
   16.46    {F (post ` M)}" |
   16.47 @@ -142,7 +142,7 @@
   16.48  "step S (SKIP {P}) = (SKIP {S})" |
   16.49  "step S (x ::= e {P}) =
   16.50    (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
   16.51 -"step S (c1; c2) = step S c1; step (post c1) c2" |
   16.52 +"step S (c1;; c2) = step S c1;; step (post c1) c2" |
   16.53  "step S (IF b THEN c1 ELSE c2 {P}) =
   16.54     IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
   16.55     {post c1 \<union> post c2}" |
    17.1 --- a/src/HOL/IMP/Abs_Int_Tests.thy	Fri May 17 02:57:00 2013 +0200
    17.2 +++ b/src/HOL/IMP/Abs_Int_Tests.thy	Fri May 17 08:19:52 2013 +0200
    17.3 @@ -8,8 +8,8 @@
    17.4  
    17.5  text{* Straight line code: *}
    17.6  definition "test1_const =
    17.7 - ''y'' ::= N 7;
    17.8 - ''z'' ::= Plus (V ''y'') (N 2);
    17.9 + ''y'' ::= N 7;;
   17.10 + ''z'' ::= Plus (V ''y'') (N 2);;
   17.11   ''y'' ::= Plus (V ''x'') (N 0)"
   17.12  
   17.13  text{* Conditional: *}
   17.14 @@ -18,26 +18,26 @@
   17.15  
   17.16  text{* Conditional, test is relevant: *}
   17.17  definition "test3_const =
   17.18 - ''x'' ::= N 42;
   17.19 + ''x'' ::= N 42;;
   17.20   IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
   17.21  
   17.22  text{* While: *}
   17.23  definition "test4_const =
   17.24 - ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
   17.25 + ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
   17.26  
   17.27  text{* While, test is relevant: *}
   17.28  definition "test5_const =
   17.29 - ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
   17.30 + ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
   17.31  
   17.32  text{* Iteration is needed: *}
   17.33  definition "test6_const =
   17.34 -  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
   17.35 -  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
   17.36 +  ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
   17.37 +  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
   17.38  
   17.39  text{* For intervals: *}
   17.40  
   17.41  definition "test1_ivl =
   17.42 - ''y'' ::= N 7;
   17.43 + ''y'' ::= N 7;;
   17.44   IF Less (V ''x'') (V ''y'')
   17.45   THEN ''y'' ::= Plus (V ''y'') (V ''x'')
   17.46   ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
   17.47 @@ -47,22 +47,22 @@
   17.48   DO ''x'' ::= Plus (V ''x'') (N 1)"
   17.49  
   17.50  definition "test3_ivl =
   17.51 - ''x'' ::= N 7;
   17.52 + ''x'' ::= N 7;;
   17.53   WHILE Less (V ''x'') (N 100)
   17.54   DO ''x'' ::= Plus (V ''x'') (N 1)"
   17.55  
   17.56  definition "test4_ivl =
   17.57 - ''x'' ::= N 0; ''y'' ::= N 0;
   17.58 + ''x'' ::= N 0;; ''y'' ::= N 0;;
   17.59   WHILE Less (V ''x'') (N 11)
   17.60 - DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N 1))"
   17.61 + DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N 1))"
   17.62  
   17.63  definition "test5_ivl =
   17.64 - ''x'' ::= N 0; ''y'' ::= N 0;
   17.65 + ''x'' ::= N 0;; ''y'' ::= N 0;;
   17.66   WHILE Less (V ''x'') (N 1000)
   17.67 - DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
   17.68 + DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
   17.69  
   17.70  definition "test6_ivl =
   17.71 - ''x'' ::= N 0;
   17.72 + ''x'' ::= N 0;;
   17.73   WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
   17.74  
   17.75  end
    18.1 --- a/src/HOL/IMP/Big_Step.thy	Fri May 17 02:57:00 2013 +0200
    18.2 +++ b/src/HOL/IMP/Big_Step.thy	Fri May 17 08:19:52 2013 +0200
    18.3 @@ -11,7 +11,7 @@
    18.4  Skip:    "(SKIP,s) \<Rightarrow> s" |
    18.5  Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
    18.6  Seq:     "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
    18.7 -          (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    18.8 +          (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    18.9  
   18.10  IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   18.11            (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   18.12 @@ -24,7 +24,7 @@
   18.13  text_raw{*}%endsnip*}
   18.14  
   18.15  text_raw{*\snip{BigStepEx}{1}{2}{% *}
   18.16 -schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
   18.17 +schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
   18.18  apply(rule Seq)
   18.19  apply(rule Assign)
   18.20  apply simp
   18.21 @@ -89,7 +89,7 @@
   18.22  
   18.23  inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
   18.24  thm AssignE
   18.25 -inductive_cases SeqE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
   18.26 +inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
   18.27  thm SeqE
   18.28  inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
   18.29  thm IfE
   18.30 @@ -143,7 +143,7 @@
   18.31    transformation on programs:
   18.32  *}
   18.33  lemma unfold_while:
   18.34 -  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
   18.35 +  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
   18.36  proof -
   18.37    -- "to show the equivalence, we look at the derivation tree for"
   18.38    -- "each side and from that construct a derivation tree for the other side"
   18.39 @@ -162,7 +162,7 @@
   18.40          "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
   18.41        -- "now we can build a derivation tree for the @{text IF}"
   18.42        -- "first, the body of the True-branch:"
   18.43 -      hence "(c; ?w, s) \<Rightarrow> t" by (rule Seq)
   18.44 +      hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
   18.45        -- "then the whole @{text IF}"
   18.46        with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
   18.47      }
   18.48 @@ -183,7 +183,7 @@
   18.49      -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
   18.50      -- {* then this time only the @{text IfTrue} rule can have be used *}
   18.51      { assume "bval b s"
   18.52 -      with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
   18.53 +      with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto
   18.54        -- "and for this, only the Seq-rule is applicable:"
   18.55        then obtain s' where
   18.56          "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
   18.57 @@ -203,7 +203,7 @@
   18.58  prove many such facts automatically.  *}
   18.59  
   18.60  lemma while_unfold:
   18.61 -  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
   18.62 +  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)"
   18.63  by blast
   18.64  
   18.65  lemma triv_if:
    19.1 --- a/src/HOL/IMP/Collecting.thy	Fri May 17 02:57:00 2013 +0200
    19.2 +++ b/src/HOL/IMP/Collecting.thy	Fri May 17 08:19:52 2013 +0200
    19.3 @@ -19,7 +19,7 @@
    19.4  "Step S (SKIP {Q}) = (SKIP {S})" |
    19.5  "Step S (x ::= e {Q}) =
    19.6    x ::= e {f x e S}" |
    19.7 -"Step S (C1; C2) = Step S C1; Step (post C1) C2" |
    19.8 +"Step S (C1;; C2) = Step S C1;; Step (post C1) C2" |
    19.9  "Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
   19.10    IF b THEN {g b S} Step P1 C1 ELSE {g (Not b) S} Step P2 C2
   19.11    {post C1 \<squnion> post C2}" |
   19.12 @@ -69,7 +69,7 @@
   19.13  lemma Assign_le[simp]: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
   19.14  by (cases c) (auto simp:less_eq_acom_def anno_def)
   19.15  
   19.16 -lemma Seq_le[simp]: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
   19.17 +lemma Seq_le[simp]: "C1;;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';;C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
   19.18  apply (cases C)
   19.19  apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
   19.20  done
    20.1 --- a/src/HOL/IMP/Com.thy	Fri May 17 02:57:00 2013 +0200
    20.2 +++ b/src/HOL/IMP/Com.thy	Fri May 17 08:19:52 2013 +0200
    20.3 @@ -5,7 +5,7 @@
    20.4  datatype
    20.5    com = SKIP 
    20.6        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
    20.7 -      | Seq    com  com         ("_;/ _"  [60, 61] 60)
    20.8 +      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
    20.9        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   20.10        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   20.11  
    21.1 --- a/src/HOL/IMP/Compiler.thy	Fri May 17 02:57:00 2013 +0200
    21.2 +++ b/src/HOL/IMP/Compiler.thy	Fri May 17 08:19:52 2013 +0200
    21.3 @@ -209,7 +209,7 @@
    21.4  fun ccomp :: "com \<Rightarrow> instr list" where
    21.5  "ccomp SKIP = []" |
    21.6  "ccomp (x ::= a) = acomp a @ [STORE x]" |
    21.7 -"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
    21.8 +"ccomp (c\<^isub>1;;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
    21.9  "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
   21.10    (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
   21.11     in cb @ cc\<^isub>1 @ JMP (size cc\<^isub>2) # cc\<^isub>2)" |
    22.1 --- a/src/HOL/IMP/Def_Init.thy	Fri May 17 02:57:00 2013 +0200
    22.2 +++ b/src/HOL/IMP/Def_Init.thy	Fri May 17 08:19:52 2013 +0200
    22.3 @@ -7,7 +7,7 @@
    22.4  inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
    22.5  Skip: "D A SKIP A" |
    22.6  Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
    22.7 -Seq: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
    22.8 +Seq: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1;; c\<^isub>2) A\<^isub>3" |
    22.9  If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
   22.10    D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
   22.11  While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
   22.12 @@ -15,7 +15,7 @@
   22.13  inductive_cases [elim!]:
   22.14  "D A SKIP A'"
   22.15  "D A (x ::= a) A'"
   22.16 -"D A (c1;c2) A'"
   22.17 +"D A (c1;;c2) A'"
   22.18  "D A (IF b THEN c1 ELSE c2) A'"
   22.19  "D A (WHILE b DO c) A'"
   22.20  
    23.1 --- a/src/HOL/IMP/Def_Init_Big.thy	Fri May 17 02:57:00 2013 +0200
    23.2 +++ b/src/HOL/IMP/Def_Init_Big.thy	Fri May 17 08:19:52 2013 +0200
    23.3 @@ -13,7 +13,7 @@
    23.4  Skip: "(SKIP,s) \<Rightarrow> s" |
    23.5  AssignNone: "aval a s = None \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> None" |
    23.6  Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> Some(s(x := Some i))" |
    23.7 -Seq:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    23.8 +Seq:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;;c\<^isub>2,s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    23.9  
   23.10  IfNone:  "bval b s = None \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> None" |
   23.11  IfTrue:  "\<lbrakk> bval b s = Some True;  (c\<^isub>1,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
    24.1 --- a/src/HOL/IMP/Def_Init_Small.thy	Fri May 17 02:57:00 2013 +0200
    24.2 +++ b/src/HOL/IMP/Def_Init_Small.thy	Fri May 17 08:19:52 2013 +0200
    24.3 @@ -11,13 +11,13 @@
    24.4  where
    24.5  Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
    24.6  
    24.7 -Seq1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
    24.8 -Seq2:   "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
    24.9 +Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
   24.10 +Seq2:   "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';;c\<^isub>2,s')" |
   24.11  
   24.12  IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
   24.13  IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
   24.14  
   24.15 -While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
   24.16 +While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
   24.17  
   24.18  lemmas small_step_induct = small_step.induct[split_format(complete)]
   24.19  
    25.1 --- a/src/HOL/IMP/Def_Init_Sound_Small.thy	Fri May 17 02:57:00 2013 +0200
    25.2 +++ b/src/HOL/IMP/Def_Init_Sound_Small.thy	Fri May 17 08:19:52 2013 +0200
    25.3 @@ -40,7 +40,7 @@
    25.4    then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
    25.5    moreover
    25.6    then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
    25.7 -  ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
    25.8 +  ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
    25.9      by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
   25.10    thus ?case by (metis D_incr `A = dom s`)
   25.11  next
    26.1 --- a/src/HOL/IMP/Denotation.thy	Fri May 17 02:57:00 2013 +0200
    26.2 +++ b/src/HOL/IMP/Denotation.thy	Fri May 17 08:19:52 2013 +0200
    26.3 @@ -14,7 +14,7 @@
    26.4  fun C :: "com \<Rightarrow> com_den" where
    26.5  "C SKIP   = Id" |
    26.6  "C (x ::= a) = {(s,t). t = s(x := aval a s)}" |
    26.7 -"C (c0;c1)   = C(c0) O C(c1)" |
    26.8 +"C (c0;;c1)   = C(c0) O C(c1)" |
    26.9  "C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>
   26.10                              {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |
   26.11  "C(WHILE b DO c) = lfp (Gamma b (C c))"
   26.12 @@ -23,7 +23,7 @@
   26.13  lemma Gamma_mono: "mono (Gamma b c)"
   26.14  by (unfold Gamma_def mono_def) fast
   26.15  
   26.16 -lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"
   26.17 +lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;;WHILE b DO c ELSE SKIP)"
   26.18  apply simp
   26.19  apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
   26.20  apply (simp add: Gamma_def)
    27.1 --- a/src/HOL/IMP/Finite_Reachable.thy	Fri May 17 02:57:00 2013 +0200
    27.2 +++ b/src/HOL/IMP/Finite_Reachable.thy	Fri May 17 08:19:52 2013 +0200
    27.3 @@ -43,14 +43,14 @@
    27.4  by(auto simp: reachable_def dest:Assign_starD)
    27.5  
    27.6  
    27.7 -lemma Seq_stepsnD: "(c1; c2, s) \<rightarrow>(n) (c', t) \<Longrightarrow>
    27.8 -  (\<exists>c1' m. c' = c1'; c2 \<and> (c1, s) \<rightarrow>(m) (c1', t) \<and> m \<le> n) \<or>
    27.9 +lemma Seq_stepsnD: "(c1;; c2, s) \<rightarrow>(n) (c', t) \<Longrightarrow>
   27.10 +  (\<exists>c1' m. c' = c1';; c2 \<and> (c1, s) \<rightarrow>(m) (c1', t) \<and> m \<le> n) \<or>
   27.11    (\<exists>s2 m1 m2. (c1,s) \<rightarrow>(m1) (SKIP,s2) \<and> (c2, s2) \<rightarrow>(m2) (c', t) \<and> m1+m2 < n)"
   27.12  proof(induction n arbitrary: c1 c2 s)
   27.13    case 0 thus ?case by auto
   27.14  next
   27.15    case (Suc n)
   27.16 -  from Suc.prems obtain s' c12' where "(c1;c2, s) \<rightarrow> (c12', s')"
   27.17 +  from Suc.prems obtain s' c12' where "(c1;;c2, s) \<rightarrow> (c12', s')"
   27.18      and n: "(c12',s') \<rightarrow>(n) (c',t)" by auto
   27.19    from this(1) show ?case
   27.20    proof
   27.21 @@ -59,14 +59,14 @@
   27.22        using n by auto
   27.23      thus ?case by blast
   27.24    next
   27.25 -    fix c1' s'' assume 1: "(c12', s') = (c1'; c2, s'')" "(c1, s) \<rightarrow> (c1', s'')"
   27.26 -    hence n': "(c1';c2,s') \<rightarrow>(n) (c',t)" using n by auto
   27.27 +    fix c1' s'' assume 1: "(c12', s') = (c1';; c2, s'')" "(c1, s) \<rightarrow> (c1', s'')"
   27.28 +    hence n': "(c1';;c2,s') \<rightarrow>(n) (c',t)" using n by auto
   27.29      from Suc.IH[OF n'] show ?case
   27.30      proof
   27.31 -      assume "\<exists>c1'' m. c' = c1''; c2 \<and> (c1', s') \<rightarrow>(m) (c1'', t) \<and> m \<le> n"
   27.32 +      assume "\<exists>c1'' m. c' = c1'';; c2 \<and> (c1', s') \<rightarrow>(m) (c1'', t) \<and> m \<le> n"
   27.33          (is "\<exists> a b. ?P a b")
   27.34        then obtain c1'' m where 2: "?P c1'' m" by blast
   27.35 -      hence "c' = c1'';c2 \<and> (c1, s) \<rightarrow>(Suc m) (c1'',t) \<and> Suc m \<le> Suc n"
   27.36 +      hence "c' = c1'';;c2 \<and> (c1, s) \<rightarrow>(Suc m) (c1'',t) \<and> Suc m \<le> Suc n"
   27.37          using 1 by auto
   27.38        thus ?case by blast
   27.39      next
   27.40 @@ -80,13 +80,13 @@
   27.41    qed
   27.42  qed
   27.43  
   27.44 -corollary Seq_starD: "(c1; c2, s) \<rightarrow>* (c', t) \<Longrightarrow>
   27.45 -  (\<exists>c1'. c' = c1'; c2 \<and> (c1, s) \<rightarrow>* (c1', t)) \<or>
   27.46 +corollary Seq_starD: "(c1;; c2, s) \<rightarrow>* (c', t) \<Longrightarrow>
   27.47 +  (\<exists>c1'. c' = c1';; c2 \<and> (c1, s) \<rightarrow>* (c1', t)) \<or>
   27.48    (\<exists>s2. (c1,s) \<rightarrow>* (SKIP,s2) \<and> (c2, s2) \<rightarrow>* (c', t))"
   27.49  by(metis Seq_stepsnD star_if_stepsn stepsn_if_star)
   27.50  
   27.51 -lemma reachable_Seq: "reachable (c1;c2) \<subseteq>
   27.52 -  (\<lambda>c1'. c1';c2) ` reachable c1 \<union> reachable c2"
   27.53 +lemma reachable_Seq: "reachable (c1;;c2) \<subseteq>
   27.54 +  (\<lambda>c1'. c1';;c2) ` reachable c1 \<union> reachable c2"
   27.55  by(auto simp: reachable_def image_def dest!: Seq_starD)
   27.56  
   27.57  
   27.58 @@ -100,8 +100,8 @@
   27.59  
   27.60  
   27.61  lemma While_stepsnD: "(WHILE b DO c, s) \<rightarrow>(n) (c2,t) \<Longrightarrow>
   27.62 -  c2 \<in> {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP}
   27.63 -  \<or> (\<exists>c1. c2 = c1 ; WHILE b DO c \<and> (\<exists> s1 s2. (c,s1) \<rightarrow>* (c1,s2)))"
   27.64 +  c2 \<in> {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP}
   27.65 +  \<or> (\<exists>c1. c2 = c1 ;; WHILE b DO c \<and> (\<exists> s1 s2. (c,s1) \<rightarrow>* (c1,s2)))"
   27.66  proof(induction n arbitrary: s rule: less_induct)
   27.67    case (less n1)
   27.68    show ?case
   27.69 @@ -110,7 +110,7 @@
   27.70    next
   27.71      case (Suc n2)
   27.72      let ?w = "WHILE b DO c"
   27.73 -    let ?iw = "IF b THEN c ; ?w ELSE SKIP"
   27.74 +    let ?iw = "IF b THEN c ;; ?w ELSE SKIP"
   27.75      from Suc less.prems have n2: "(?iw,s) \<rightarrow>(n2) (c2,t)" by(auto elim!: WhileE)
   27.76      show ?thesis
   27.77      proof(cases n2)
   27.78 @@ -122,11 +122,11 @@
   27.79        from this(1)
   27.80        show ?thesis
   27.81        proof
   27.82 -        assume "(iw', s') = (c; WHILE b DO c, s)"
   27.83 -        with n3 have "(c;?w, s) \<rightarrow>(n3) (c2,t)" by auto
   27.84 +        assume "(iw', s') = (c;; WHILE b DO c, s)"
   27.85 +        with n3 have "(c;;?w, s) \<rightarrow>(n3) (c2,t)" by auto
   27.86          from Seq_stepsnD[OF this] show ?thesis
   27.87          proof
   27.88 -          assume "\<exists>c1' m. c2 = c1'; ?w \<and> (c,s) \<rightarrow>(m) (c1', t) \<and> m \<le> n3"
   27.89 +          assume "\<exists>c1' m. c2 = c1';; ?w \<and> (c,s) \<rightarrow>(m) (c1', t) \<and> m \<le> n3"
   27.90            thus ?thesis by (metis star_if_stepsn)
   27.91          next
   27.92            assume "\<exists>s2 m1 m2. (c, s) \<rightarrow>(m1) (SKIP, s2) \<and>
   27.93 @@ -144,8 +144,8 @@
   27.94  qed
   27.95  
   27.96  lemma reachable_While: "reachable (WHILE b DO c) \<subseteq>
   27.97 -  {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP} \<union>
   27.98 -  (\<lambda>c'. c' ; WHILE b DO c) ` reachable c"
   27.99 +  {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP} \<union>
  27.100 +  (\<lambda>c'. c' ;; WHILE b DO c) ` reachable c"
  27.101  apply(auto simp: reachable_def image_def)
  27.102  by (metis While_stepsnD insertE singletonE stepsn_if_star)
  27.103  
    28.1 --- a/src/HOL/IMP/Fold.thy	Fri May 17 02:57:00 2013 +0200
    28.2 +++ b/src/HOL/IMP/Fold.thy	Fri May 17 08:19:52 2013 +0200
    28.3 @@ -33,7 +33,7 @@
    28.4  primrec lnames :: "com \<Rightarrow> vname set" where
    28.5  "lnames SKIP = {}" |
    28.6  "lnames (x ::= a) = {x}" |
    28.7 -"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
    28.8 +"lnames (c1;; c2) = lnames c1 \<union> lnames c2" |
    28.9  "lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
   28.10  "lnames (WHILE b DO c) = lnames c"
   28.11  
   28.12 @@ -41,14 +41,14 @@
   28.13  "defs SKIP t = t" |
   28.14  "defs (x ::= a) t =
   28.15    (case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
   28.16 -"defs (c1;c2) t = (defs c2 o defs c1) t" |
   28.17 +"defs (c1;;c2) t = (defs c2 o defs c1) t" |
   28.18  "defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
   28.19  "defs (WHILE b DO c) t = t |` (-lnames c)"
   28.20  
   28.21  primrec fold where
   28.22  "fold SKIP _ = SKIP" |
   28.23  "fold (x ::= a) t = (x ::= (afold a t))" |
   28.24 -"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
   28.25 +"fold (c1;;c2) t = (fold c1 t;; fold c2 (defs c1 t))" |
   28.26  "fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
   28.27  "fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
   28.28  
   28.29 @@ -259,7 +259,7 @@
   28.30  "bdefs SKIP t = t" |
   28.31  "bdefs (x ::= a) t =
   28.32    (case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
   28.33 -"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
   28.34 +"bdefs (c1;;c2) t = (bdefs c2 o bdefs c1) t" |
   28.35  "bdefs (IF b THEN c1 ELSE c2) t = (case bfold b t of
   28.36      Bc True \<Rightarrow> bdefs c1 t
   28.37    | Bc False \<Rightarrow> bdefs c2 t
   28.38 @@ -270,7 +270,7 @@
   28.39  primrec fold' where
   28.40  "fold' SKIP _ = SKIP" |
   28.41  "fold' (x ::= a) t = (x ::= (afold a t))" |
   28.42 -"fold' (c1;c2) t = (fold' c1 t; fold' c2 (bdefs c1 t))" |
   28.43 +"fold' (c1;;c2) t = (fold' c1 t;; fold' c2 (bdefs c1 t))" |
   28.44  "fold' (IF b THEN c1 ELSE c2) t = (case bfold b t of
   28.45      Bc True \<Rightarrow> fold' c1 t
   28.46    | Bc False \<Rightarrow> fold' c2 t
    29.1 --- a/src/HOL/IMP/Hoare.thy	Fri May 17 02:57:00 2013 +0200
    29.2 +++ b/src/HOL/IMP/Hoare.thy	Fri May 17 08:19:52 2013 +0200
    29.3 @@ -20,7 +20,7 @@
    29.4  Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    29.5  
    29.6  Seq: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
    29.7 -      \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
    29.8 +      \<Longrightarrow> \<turnstile> {P} c\<^isub>1;;c\<^isub>2 {R}"  |
    29.9  
   29.10  If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q};  \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
   29.11       \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
    30.1 --- a/src/HOL/IMP/HoareT.thy	Fri May 17 02:57:00 2013 +0200
    30.2 +++ b/src/HOL/IMP/HoareT.thy	Fri May 17 08:19:52 2013 +0200
    30.3 @@ -22,7 +22,7 @@
    30.4  where
    30.5  Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}" |
    30.6  Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
    30.7 -Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" |
    30.8 +Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;;c\<^isub>2 {P\<^isub>3}" |
    30.9  If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
   30.10    \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
   30.11  While:
   30.12 @@ -56,9 +56,9 @@
   30.13  
   30.14  abbreviation "w n ==
   30.15    WHILE Less (V ''y'') (N n)
   30.16 -  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
   30.17 +  DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
   30.18  
   30.19 -lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
   30.20 +lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
   30.21  apply(rule Seq)
   30.22  prefer 2
   30.23  apply(rule While'
   30.24 @@ -112,7 +112,7 @@
   30.25  lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
   30.26  by(auto intro!: ext simp: wpt_def)
   30.27  
   30.28 -lemma [simp]: "wp\<^sub>t (c\<^isub>1;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
   30.29 +lemma [simp]: "wp\<^sub>t (c\<^isub>1;;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
   30.30  unfolding wpt_def
   30.31  apply(rule ext)
   30.32  apply auto
    31.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Fri May 17 02:57:00 2013 +0200
    31.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Fri May 17 08:19:52 2013 +0200
    31.3 @@ -9,7 +9,7 @@
    31.4  
    31.5  abbreviation "w n ==
    31.6    WHILE Less (V ''y'') (N n)
    31.7 -  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
    31.8 +  DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
    31.9  
   31.10  text{* For this example we make use of some predefined functions.  Function
   31.11  @{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
   31.12 @@ -37,7 +37,7 @@
   31.13  Now we prefix the loop with the necessary initialization: *}
   31.14  
   31.15  lemma sum_via_bigstep:
   31.16 -assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) \<Rightarrow> t"
   31.17 +assumes "(''x'' ::= N 0;; ''y'' ::= N 0;; w n, s) \<Rightarrow> t"
   31.18  shows "t ''x'' = \<Sum> {1 .. n}"
   31.19  proof -
   31.20    from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
   31.21 @@ -50,7 +50,7 @@
   31.22  text{* Note that we deal with sequences of commands from right to left,
   31.23  pulling back the postcondition towards the precondition. *}
   31.24  
   31.25 -lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
   31.26 +lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
   31.27  apply(rule hoare.Seq)
   31.28  prefer 2
   31.29  apply(rule While'
    32.1 --- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Fri May 17 02:57:00 2013 +0200
    32.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Fri May 17 08:19:52 2013 +0200
    32.3 @@ -35,7 +35,7 @@
    32.4  lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
    32.5  by (rule ext) (auto simp: wp_def)
    32.6  
    32.7 -lemma wp_Seq[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
    32.8 +lemma wp_Seq[simp]: "wp (c\<^isub>1;;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
    32.9  by (rule ext) (auto simp: wp_def)
   32.10  
   32.11  lemma wp_If[simp]:
   32.12 @@ -45,11 +45,11 @@
   32.13  
   32.14  lemma wp_While_If:
   32.15   "wp (WHILE b DO c) Q s =
   32.16 -  wp (IF b THEN c;WHILE b DO c ELSE SKIP) Q s"
   32.17 +  wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
   32.18  unfolding wp_def by (metis unfold_while)
   32.19  
   32.20  lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
   32.21 -  wp (WHILE b DO c) Q s = wp (c; WHILE b DO c) Q s"
   32.22 +  wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
   32.23  by(simp add: wp_While_If)
   32.24  
   32.25  lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
    33.1 --- a/src/HOL/IMP/Live.thy	Fri May 17 02:57:00 2013 +0200
    33.2 +++ b/src/HOL/IMP/Live.thy	Fri May 17 08:19:52 2013 +0200
    33.3 @@ -10,25 +10,25 @@
    33.4  fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
    33.5  "L SKIP X = X" |
    33.6  "L (x ::= a) X = vars a \<union> (X - {x})" |
    33.7 -"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
    33.8 +"L (c\<^isub>1;; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
    33.9  "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
   33.10  "L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
   33.11  
   33.12 -value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
   33.13 +value "show (L (''y'' ::= V ''z'';; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
   33.14  
   33.15  value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
   33.16  
   33.17  fun "kill" :: "com \<Rightarrow> vname set" where
   33.18  "kill SKIP = {}" |
   33.19  "kill (x ::= a) = {x}" |
   33.20 -"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
   33.21 +"kill (c\<^isub>1;; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
   33.22  "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
   33.23  "kill (WHILE b DO c) = {}"
   33.24  
   33.25  fun gen :: "com \<Rightarrow> vname set" where
   33.26  "gen SKIP = {}" |
   33.27  "gen (x ::= a) = vars a" |
   33.28 -"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
   33.29 +"gen (c\<^isub>1;; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
   33.30  "gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
   33.31  "gen (WHILE b DO c) = vars b \<union> gen c"
   33.32  
   33.33 @@ -110,7 +110,7 @@
   33.34  fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
   33.35  "bury SKIP X = SKIP" |
   33.36  "bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" |
   33.37 -"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
   33.38 +"bury (c\<^isub>1;; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X);; bury c\<^isub>2 X)" |
   33.39  "bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
   33.40  "bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)"
   33.41  
   33.42 @@ -182,8 +182,8 @@
   33.43  lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
   33.44  by (cases c) auto
   33.45  
   33.46 -lemma Seq_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
   33.47 -  (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
   33.48 +lemma Seq_bury[simp]: "bc\<^isub>1;;bc\<^isub>2 = bury c X \<longleftrightarrow>
   33.49 +  (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
   33.50  by (cases c) auto
   33.51  
   33.52  lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
   33.53 @@ -205,7 +205,7 @@
   33.54      by (auto simp: ball_Un)
   33.55  next
   33.56    case (Seq bc1 s1 s2 bc2 s3 c X t1)
   33.57 -  then obtain c1 c2 where c: "c = c1;c2"
   33.58 +  then obtain c1 c2 where c: "c = c1;;c2"
   33.59      and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
   33.60    note IH = Seq.hyps(2,4)
   33.61    from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
    34.1 --- a/src/HOL/IMP/Live_True.thy	Fri May 17 02:57:00 2013 +0200
    34.2 +++ b/src/HOL/IMP/Live_True.thy	Fri May 17 08:19:52 2013 +0200
    34.3 @@ -9,7 +9,7 @@
    34.4  fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
    34.5  "L SKIP X = X" |
    34.6  "L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" |
    34.7 -"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
    34.8 +"L (c\<^isub>1;; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
    34.9  "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
   34.10  "L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"
   34.11  
   34.12 @@ -154,7 +154,7 @@
   34.13  text{* Sorry, this syntax is odd. *}
   34.14  
   34.15  text{* A test: *}
   34.16 -lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x''; ''x'' ::= V ''z''
   34.17 +lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x'';; ''x'' ::= V ''z''
   34.18    in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}"
   34.19  by eval
   34.20  
   34.21 @@ -173,12 +173,12 @@
   34.22  fun Lb :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
   34.23  "Lb SKIP X = X" |
   34.24  "Lb (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
   34.25 -"Lb (c\<^isub>1; c\<^isub>2) X = (Lb c\<^isub>1 \<circ> Lb c\<^isub>2) X" |
   34.26 +"Lb (c\<^isub>1;; c\<^isub>2) X = (Lb c\<^isub>1 \<circ> Lb c\<^isub>2) X" |
   34.27  "Lb (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> Lb c\<^isub>1 X \<union> Lb c\<^isub>2 X" |
   34.28  "Lb (WHILE b DO c) X = iter (\<lambda>A. vars b \<union> X \<union> Lb c A) 2 {} (vars b \<union> vars c \<union> X)"
   34.29  
   34.30  text{* @{const Lb} (and @{const iter}) is not monotone! *}
   34.31 -lemma "let w = WHILE Bc False DO (''x'' ::= V ''y''; ''z'' ::= V ''x'')
   34.32 +lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'')
   34.33    in \<not> (Lb w {''z''} \<subseteq> Lb w {''y'',''z''})"
   34.34  by eval
   34.35  
    35.1 --- a/src/HOL/IMP/Poly_Types.thy	Fri May 17 02:57:00 2013 +0200
    35.2 +++ b/src/HOL/IMP/Poly_Types.thy	Fri May 17 08:19:52 2013 +0200
    35.3 @@ -26,7 +26,7 @@
    35.4  inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>p" 50) where
    35.5  "\<Gamma> \<turnstile>p SKIP" |
    35.6  "\<Gamma> \<turnstile>p a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile>p x ::= a" |
    35.7 -"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;c2" |
    35.8 +"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;;c2" |
    35.9  "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p IF b THEN c1 ELSE c2" |
   35.10  "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c \<Longrightarrow> \<Gamma> \<turnstile>p WHILE b DO c"
   35.11  
    36.1 --- a/src/HOL/IMP/Procs.thy	Fri May 17 02:57:00 2013 +0200
    36.2 +++ b/src/HOL/IMP/Procs.thy	Fri May 17 08:19:52 2013 +0200
    36.3 @@ -9,20 +9,20 @@
    36.4  datatype
    36.5    com = SKIP 
    36.6        | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
    36.7 -      | Seq    com  com          ("_;/ _"  [60, 61] 60)
    36.8 +      | Seq    com  com          ("_;;/ _"  [60, 61] 60)
    36.9        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   36.10        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   36.11 -      | Var    vname com        ("(1{VAR _;;/ _})")
   36.12 -      | Proc   pname com com    ("(1{PROC _ = _;;/ _})")
   36.13 +      | Var    vname com        ("(1{VAR _;/ _})")
   36.14 +      | Proc   pname com com    ("(1{PROC _ = _;/ _})")
   36.15        | CALL   pname
   36.16  
   36.17  definition "test_com =
   36.18 -{VAR ''x'';;
   36.19 - {PROC ''p'' = ''x'' ::= N 1;;
   36.20 -  {PROC ''q'' = CALL ''p'';;
   36.21 -   {VAR ''x'';;
   36.22 -    ''x'' ::= N 2;
   36.23 -    {PROC ''p'' = ''x'' ::= N 3;;
   36.24 -     CALL ''q''; ''y'' ::= V ''x''}}}}}"
   36.25 +{VAR ''x'';
   36.26 + {PROC ''p'' = ''x'' ::= N 1;
   36.27 +  {PROC ''q'' = CALL ''p'';
   36.28 +   {VAR ''x'';
   36.29 +    ''x'' ::= N 2;;
   36.30 +    {PROC ''p'' = ''x'' ::= N 3;
   36.31 +     CALL ''q'';; ''y'' ::= V ''x''}}}}}"
   36.32  
   36.33  end
    37.1 --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Fri May 17 02:57:00 2013 +0200
    37.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Fri May 17 08:19:52 2013 +0200
    37.3 @@ -11,7 +11,7 @@
    37.4  Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
    37.5  Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
    37.6  Seq:     "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
    37.7 -          pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    37.8 +          pe \<turnstile> (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    37.9  
   37.10  IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   37.11           pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   37.12 @@ -23,11 +23,11 @@
   37.13    "\<lbrakk> bval b s\<^isub>1;  pe \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
   37.14     pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   37.15  
   37.16 -Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
   37.17 +Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x; c}, s) \<Rightarrow> t(x := s x)" |
   37.18  
   37.19  Call: "pe \<turnstile> (pe p, s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
   37.20  
   37.21 -Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
   37.22 +Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
   37.23  
   37.24  code_pred big_step .
   37.25  
    38.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Fri May 17 02:57:00 2013 +0200
    38.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Fri May 17 08:19:52 2013 +0200
    38.3 @@ -11,7 +11,7 @@
    38.4  Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
    38.5  Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
    38.6  Seq:     "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
    38.7 -          pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    38.8 +          pe \<turnstile> (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    38.9  
   38.10  IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   38.11           pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   38.12 @@ -23,13 +23,13 @@
   38.13    "\<lbrakk> bval b s\<^isub>1;  pe \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
   38.14     pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   38.15  
   38.16 -Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
   38.17 +Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x; c}, s) \<Rightarrow> t(x := s x)" |
   38.18  
   38.19  Call1: "(p,c)#pe \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>  (p,c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
   38.20  Call2: "\<lbrakk> p' \<noteq> p;  pe \<turnstile> (CALL p, s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   38.21         (p',c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
   38.22  
   38.23 -Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
   38.24 +Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
   38.25  
   38.26  code_pred big_step .
   38.27  
    39.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Fri May 17 02:57:00 2013 +0200
    39.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Fri May 17 08:19:52 2013 +0200
    39.3 @@ -18,7 +18,7 @@
    39.4  Skip:    "e \<turnstile> (SKIP,s) \<Rightarrow> s" |
    39.5  Assign:  "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" |
    39.6  Seq:     "\<lbrakk> e \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  e \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
    39.7 -          e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    39.8 +          e \<turnstile> (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
    39.9  
   39.10  IfTrue:  "\<lbrakk> bval b (s \<circ> venv e);  e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   39.11           e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   39.12 @@ -32,7 +32,7 @@
   39.13     e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   39.14  
   39.15  Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>
   39.16 -      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t" |
   39.17 +      (pe,ve,f) \<turnstile> ({VAR x; c}, s) \<Rightarrow> t" |
   39.18  
   39.19  Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>
   39.20          ((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
   39.21 @@ -40,7 +40,7 @@
   39.22         ((p',c,ve')#pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
   39.23  
   39.24  Proc: "((p,cp,ve)#pe,ve,f) \<turnstile> (c,s) \<Rightarrow> t
   39.25 -      \<Longrightarrow>  (pe,ve,f) \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
   39.26 +      \<Longrightarrow>  (pe,ve,f) \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
   39.27  
   39.28  code_pred big_step .
   39.29  
    40.1 --- a/src/HOL/IMP/Sec_Typing.thy	Fri May 17 02:57:00 2013 +0200
    40.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Fri May 17 08:19:52 2013 +0200
    40.3 @@ -11,7 +11,7 @@
    40.4  Assign:
    40.5    "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
    40.6  Seq:
    40.7 -  "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
    40.8 +  "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2" |
    40.9  If:
   40.10    "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
   40.11  While:
   40.12 @@ -24,7 +24,7 @@
   40.13  value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
   40.14  
   40.15  inductive_cases [elim!]:
   40.16 -  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
   40.17 +  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
   40.18  
   40.19  
   40.20  text{* An important property: anti-monotonicity. *}
   40.21 @@ -187,7 +187,7 @@
   40.22  Assign':
   40.23    "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
   40.24  Seq':
   40.25 -  "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
   40.26 +  "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" |
   40.27  If':
   40.28    "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
   40.29  While':
   40.30 @@ -221,7 +221,7 @@
   40.31  Assign2:
   40.32    "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
   40.33  Seq2:
   40.34 -  "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " |
   40.35 +  "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " |
   40.36  If2:
   40.37    "\<lbrakk> sec b \<le> min l\<^isub>1 l\<^isub>2;  \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
   40.38    \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
    41.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Fri May 17 02:57:00 2013 +0200
    41.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Fri May 17 08:19:52 2013 +0200
    41.3 @@ -9,7 +9,7 @@
    41.4  Assign:
    41.5    "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
    41.6  Seq:
    41.7 -  "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
    41.8 +  "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2"  |
    41.9  If:
   41.10    "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk>
   41.11     \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
   41.12 @@ -19,7 +19,7 @@
   41.13  code_pred (expected_modes: i => i => bool) sec_type .
   41.14  
   41.15  inductive_cases [elim!]:
   41.16 -  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
   41.17 +  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
   41.18  
   41.19  
   41.20  lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
   41.21 @@ -176,7 +176,7 @@
   41.22  Assign':
   41.23    "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
   41.24  Seq':
   41.25 -  "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
   41.26 +  "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2"  |
   41.27  If':
   41.28    "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
   41.29  While':
    42.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Fri May 17 02:57:00 2013 +0200
    42.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Fri May 17 08:19:52 2013 +0200
    42.3 @@ -70,7 +70,7 @@
    42.4  lemma equiv_up_to_seq:
    42.5    "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow>
    42.6    (\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
    42.7 -  P \<Turnstile> (c; d) \<sim> (c'; d')"
    42.8 +  P \<Turnstile> (c;; d) \<sim> (c';; d')"
    42.9    by (clarsimp simp: equiv_up_to_def) blast
   42.10  
   42.11  lemma equiv_up_to_while_lemma:
    43.1 --- a/src/HOL/IMP/Small_Step.thy	Fri May 17 02:57:00 2013 +0200
    43.2 +++ b/src/HOL/IMP/Small_Step.thy	Fri May 17 08:19:52 2013 +0200
    43.3 @@ -10,14 +10,14 @@
    43.4  where
    43.5  Assign:  "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
    43.6  
    43.7 -Seq1:    "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
    43.8 -Seq2:    "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
    43.9 +Seq1:    "(SKIP;;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
   43.10 +Seq2:    "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';;c\<^isub>2,s')" |
   43.11  
   43.12  IfTrue:  "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
   43.13  IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
   43.14  
   43.15  While:   "(WHILE b DO c,s) \<rightarrow>
   43.16 -            (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
   43.17 +            (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
   43.18  text_raw{*}%endsnip*}
   43.19  
   43.20  
   43.21 @@ -30,7 +30,7 @@
   43.22  code_pred small_step .
   43.23  
   43.24  values "{(c',map t [''x'',''y'',''z'']) |c' t.
   43.25 -   (''x'' ::= V ''z''; ''y'' ::= V ''x'',
   43.26 +   (''x'' ::= V ''z'';; ''y'' ::= V ''x'',
   43.27      <''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
   43.28  
   43.29  
   43.30 @@ -56,7 +56,7 @@
   43.31  thm SkipE
   43.32  inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
   43.33  thm AssignE
   43.34 -inductive_cases SeqE[elim]: "(c1;c2,s) \<rightarrow> ct"
   43.35 +inductive_cases SeqE[elim]: "(c1;;c2,s) \<rightarrow> ct"
   43.36  thm SeqE
   43.37  inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
   43.38  inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
   43.39 @@ -72,7 +72,7 @@
   43.40  
   43.41  subsection "Equivalence with big-step semantics"
   43.42  
   43.43 -lemma star_seq2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
   43.44 +lemma star_seq2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow>* (c1';;c2,s')"
   43.45  proof(induction rule: star_induct)
   43.46    case refl thus ?case by simp
   43.47  next
   43.48 @@ -82,7 +82,7 @@
   43.49  
   43.50  lemma seq_comp:
   43.51    "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
   43.52 -   \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
   43.53 +   \<Longrightarrow> (c1;;c2, s1) \<rightarrow>* (SKIP,s3)"
   43.54  by(blast intro: star.step star_seq2 star_trans)
   43.55  
   43.56  text{* The following proof corresponds to one on the board where one would
   43.57 @@ -97,7 +97,7 @@
   43.58  next
   43.59    fix c1 c2 s1 s2 s3
   43.60    assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
   43.61 -  thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule seq_comp)
   43.62 +  thus "(c1;;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule seq_comp)
   43.63  next
   43.64    fix s::state and b c0 c1 t
   43.65    assume "bval b s"
   43.66 @@ -115,20 +115,20 @@
   43.67  next
   43.68    fix b c and s::state
   43.69    assume b: "\<not>bval b s"
   43.70 -  let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
   43.71 +  let ?if = "IF b THEN c;; WHILE b DO c ELSE SKIP"
   43.72    have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
   43.73    moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
   43.74    ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by(metis star.refl star.step)
   43.75  next
   43.76    fix b c s s' t
   43.77    let ?w  = "WHILE b DO c"
   43.78 -  let ?if = "IF b THEN c; ?w ELSE SKIP"
   43.79 +  let ?if = "IF b THEN c;; ?w ELSE SKIP"
   43.80    assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
   43.81    assume c: "(c,s) \<rightarrow>* (SKIP,s')"
   43.82    assume b: "bval b s"
   43.83    have "(?w,s) \<rightarrow> (?if, s)" by blast
   43.84 -  moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
   43.85 -  moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule seq_comp[OF c w])
   43.86 +  moreover have "(?if, s) \<rightarrow> (c;; ?w, s)" by (simp add: b)
   43.87 +  moreover have "(c;; ?w,s) \<rightarrow>* (SKIP,t)" by(rule seq_comp[OF c w])
   43.88    ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
   43.89  qed
   43.90  
    44.1 --- a/src/HOL/IMP/Types.thy	Fri May 17 02:57:00 2013 +0200
    44.2 +++ b/src/HOL/IMP/Types.thy	Fri May 17 08:19:52 2013 +0200
    44.3 @@ -44,7 +44,7 @@
    44.4  datatype
    44.5    com = SKIP 
    44.6        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
    44.7 -      | Seq    com  com         ("_; _"  [60, 61] 60)
    44.8 +      | Seq    com  com         ("_;; _"  [60, 61] 60)
    44.9        | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
   44.10        | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)
   44.11  
   44.12 @@ -56,13 +56,13 @@
   44.13  where
   44.14  Assign:  "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
   44.15  
   44.16 -Seq1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
   44.17 -Seq2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
   44.18 +Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
   44.19 +Seq2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow> (c1';;c2,s')" |
   44.20  
   44.21  IfTrue:  "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
   44.22  IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
   44.23  
   44.24 -While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
   44.25 +While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
   44.26  
   44.27  lemmas small_step_induct = small_step.induct[split_format(complete)]
   44.28  
   44.29 @@ -95,12 +95,12 @@
   44.30  inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
   44.31  Skip_ty: "\<Gamma> \<turnstile> SKIP" |
   44.32  Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
   44.33 -Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
   44.34 +Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;;c2" |
   44.35  If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
   44.36  While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
   44.37  
   44.38  inductive_cases [elim!]:
   44.39 -  "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;c2"
   44.40 +  "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;;c2"
   44.41    "\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
   44.42    "\<Gamma> \<turnstile> WHILE b DO c"
   44.43  
    45.1 --- a/src/HOL/IMP/VC.thy	Fri May 17 02:57:00 2013 +0200
    45.2 +++ b/src/HOL/IMP/VC.thy	Fri May 17 08:19:52 2013 +0200
    45.3 @@ -10,7 +10,7 @@
    45.4  datatype acom =
    45.5    ASKIP |
    45.6    Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
    45.7 -  Aseq   acom acom       ("_;/ _"  [60, 61] 60) |
    45.8 +  Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
    45.9    Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
   45.10    Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
   45.11  
   45.12 @@ -42,7 +42,7 @@
   45.13  fun strip :: "acom \<Rightarrow> com" where
   45.14  "strip ASKIP = SKIP" |
   45.15  "strip (Aassign x a) = (x::=a)" |
   45.16 -"strip (Aseq c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
   45.17 +"strip (Aseq c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1;; strip c\<^isub>2)" |
   45.18  "strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
   45.19  "strip (Awhile I b c) = (WHILE b DO strip c)"
   45.20  
    46.1 --- a/src/HOL/IMP/Vars.thy	Fri May 17 02:57:00 2013 +0200
    46.2 +++ b/src/HOL/IMP/Vars.thy	Fri May 17 08:19:52 2013 +0200
    46.3 @@ -72,9 +72,9 @@
    46.4  begin
    46.5  
    46.6  fun vars_com :: "com \<Rightarrow> vname set" where
    46.7 -"vars com.SKIP = {}" |
    46.8 +"vars SKIP = {}" |
    46.9  "vars (x::=e) = {x} \<union> vars e" |
   46.10 -"vars (c1;c2) = vars c1 \<union> vars c2" |
   46.11 +"vars (c1;;c2) = vars c1 \<union> vars c2" |
   46.12  "vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" |
   46.13  "vars (WHILE b DO c) = vars b \<union> vars c"
   46.14