# HG changeset patch
# User wenzelm
# Date 979238185 -3600
# Node ID 904cefa2c3cdbfe7a1c060e5f9971e397fc981a7
# Parent  5af3906edec837e466798525d4cc5f557e8075b7
subst syntax;

diff -r 5af3906edec8 -r 904cefa2c3cd src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Thu Jan 11 12:49:48 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Thu Jan 11 19:36:25 2001 +0100
@@ -217,10 +217,11 @@
 *}
 
 syntax
-  "_quote"       :: "'b => ('a => 'b)"        ("(.'(_').)" [0] 1000)
-  "_antiquote"   :: "('a => 'b) => 'b"        ("\<acute>_" [1000] 1000)
-  "_Assert"      :: "'a => 'a set"            ("(.{_}.)" [0] 1000)
-  "_Assign"      :: "idt => 'b => 'a com"     ("(\<acute>_ :=/ _)" [70, 65] 61)
+  "_quote"       :: "'b => ('a => 'b)"                  ("(.'(_').)" [0] 1000)
+  "_antiquote"   :: "('a => 'b) => 'b"                  ("\<acute>_" [1000] 1000)
+  "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"  ("_[_'/\<acute>_]" [1000] 999)
+  "_Assert"      :: "'a => 'a set"                      ("(.{_}.)" [0] 1000)
+  "_Assign"      :: "idt => 'b => 'a com"               ("(\<acute>_ :=/ _)" [70, 65] 61)
   "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
         ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
@@ -233,9 +234,10 @@
 
 translations
   ".{b}."                   => "Collect .(b)."
+  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x a) \<in> B}."
   "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x a))."
-  "IF b THEN c1 ELSE c2 FI" => "Cond (Collect .(b).) c1 c2"
-  "WHILE b INV i DO c OD"   => "While (Collect .(b).) i c"
+  "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
+  "WHILE b INV i DO c OD"   => "While .{b}. i c"
   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
 
 parse_translation {*
@@ -335,7 +337,7 @@
   thus ?thesis by simp
 qed
 
-lemma assign: "|- .{\<acute>(x_update \<acute>a) : P}. \<acute>x := \<acute>a P"
+lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
   by (rule basic)
 
 text {*