# HG changeset patch
# User wenzelm
# Date 979082133 -3600
# Node ID 9423817dee84283b7fa51bc9c6813789c0407a9d
# Parent  7d640de604e4f839ac5943fc4a504fc8b63dc779
use \<acute>;

diff -r 7d640de604e4 -r 9423817dee84 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Wed Jan 10 00:14:52 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Wed Jan 10 00:15:33 2001 +0100
@@ -218,9 +218,9 @@
 
 syntax
   "_quote"       :: "'b => ('a => 'b)"        ("(.'(_').)" [0] 1000)
-  "_antiquote"   :: "('a => 'b) => 'b"        ("`_" [1000] 1000)
+  "_antiquote"   :: "('a => 'b) => 'b"        ("\<acute>_" [1000] 1000)
   "_Assert"      :: "'a => 'a set"            ("(.{_}.)" [0] 1000)
-  "_Assign"      :: "idt => 'b => 'a com"     ("(`_ :=/ _)" [70, 65] 61)
+  "_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,7 +233,7 @@
 
 translations
   ".{b}."                   => "Collect .(b)."
-  "`x := a"                 => "Basic .(`(_update_name x a))."
+  "\<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"
   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
@@ -308,17 +308,17 @@
   by (unfold Valid_def) blast
 
 lemma [trans]:
-    "|- .{`P}. c Q ==> (!!s. P' s --> P s) ==> |- .{`P'}. c Q"
+    "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
   by (simp add: Valid_def)
 lemma [trans]:
-    "(!!s. P' s --> P s) ==> |- .{`P}. c Q ==> |- .{`P'}. c Q"
+    "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
   by (simp add: Valid_def)
 
 lemma [trans]:
-    "|- P c .{`Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{`Q'}."
+    "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
   by (simp add: Valid_def)
 lemma [trans]:
-    "(!!s. Q s --> Q' s) ==> |- P c .{`Q}. ==> |- P c .{`Q'}."
+    "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
   by (simp add: Valid_def)
 
 
@@ -335,7 +335,7 @@
   thus ?thesis by simp
 qed
 
-lemma assign: "|- .{`(x_update `a) : P}. `x := `a P"
+lemma assign: "|- .{\<acute>(x_update \<acute>a) : P}. \<acute>x := \<acute>a P"
   by (rule basic)
 
 text {*
@@ -345,7 +345,7 @@
  $x$, Isabelle/HOL provides a functions $x$ (selector) and
  $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
  appearing for the latter kind of function: due to concrete syntax
- \isa{`x := `a} also contains \isa{x\_update}.\footnote{Note that due
+ \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
  to the external nature of HOL record fields, we could not even state
  a general theorem relating selector and update functions (if this
  were required here); this would only work for any particular instance
@@ -369,9 +369,9 @@
 lemmas [trans, intro?] = cond
 
 lemma [trans, intro?]:
-  "|- .{`P & `b}. c1 Q
-      ==> |- .{`P & ~ `b}. c2 Q
-      ==> |- .{`P}. IF `b THEN c1 ELSE c2 FI Q"
+  "|- .{\<acute>P & \<acute>b}. c1 Q
+      ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
+      ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
     by (rule cond) (simp_all add: Valid_def)
 
 text {*
@@ -388,13 +388,13 @@
 
 
 lemma [intro?]:
-  "|- .{`P & `b}. c .{`P}.
-    ==> |- .{`P}. WHILE `b INV .{`P}. DO c OD .{`P & ~ `b}."
+  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
+    ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
   by (simp add: while Collect_conj_eq Collect_neg_eq)
 
 lemma [intro?]:
-  "|- .{`P & `b}. c .{`P}.
-    ==> |- .{`P}. WHILE `b DO c OD .{`P & ~ `b}."
+  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
+    ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
   by (simp add: while Collect_conj_eq Collect_neg_eq)
 
 
diff -r 7d640de604e4 -r 9423817dee84 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Wed Jan 10 00:14:52 2001 +0100
+++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Jan 10 00:15:33 2001 +0100
@@ -39,7 +39,7 @@
 *}
 
 lemma
-  "|- .{`(N_update (2 * `N)) : .{`N = #10}.}. `N := 2 * `N .{`N = #10}."
+  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = #10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
   by (rule assign)
 
 text {*
@@ -49,31 +49,31 @@
  ``obvious'' consequences as well.
 *}
 
-lemma "|- .{True}. `N := #10 .{`N = #10}."
+lemma "|- .{True}. \<acute>N := #10 .{\<acute>N = #10}."
   by hoare
 
-lemma "|- .{2 * `N = #10}. `N := 2 * `N .{`N = #10}."
+lemma "|- .{2 * \<acute>N = #10}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
   by hoare
 
-lemma "|- .{`N = #5}. `N := 2 * `N .{`N = #10}."
+lemma "|- .{\<acute>N = #5}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
   by hoare simp
 
-lemma "|- .{`N + 1 = a + 1}. `N := `N + 1 .{`N = a + 1}."
+lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
   by hoare
 
-lemma "|- .{`N = a}. `N := `N + 1 .{`N = a + 1}."
+lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
   by hoare simp
 
-lemma "|- .{a = a & b = b}. `M := a; `N := b .{`M = a & `N = b}."
+lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
   by hoare
 
-lemma "|- .{True}. `M := a; `N := b .{`M = a & `N = b}."
+lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
   by hoare simp
 
 lemma
-"|- .{`M = a & `N = b}.
-    `I := `M; `M := `N; `N := `I
-    .{`M = b & `N = a}."
+"|- .{\<acute>M = a & \<acute>N = b}.
+    \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
+    .{\<acute>M = b & \<acute>N = a}."
   by hoare simp
 
 text {*
@@ -83,10 +83,10 @@
  relating record selectors and updates schematically.
 *}
 
-lemma "|- .{`N = a}. `N := `N .{`N = a}."
+lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
   by hoare
 
-lemma "|- .{`x = a}. `x := `x .{`x = a}."
+lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
   oops
 
 lemma
@@ -101,27 +101,27 @@
  \name{hoare} method is able to handle this case, too.
 *}
 
-lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
 proof -
-  have ".{`M = `N}. <= .{`M + 1 ~= `N}."
+  have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
     by auto
-  also have "|- ... `M := `M + 1 .{`M ~= `N}."
+  also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
     by hoare
   finally show ?thesis .
 qed
 
-lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
 proof -
   have "!!m n. m = n --> m + 1 ~= n"
       -- {* inclusion of assertions expressed in ``pure'' logic, *}
       -- {* without mentioning the state space *}
     by simp
-  also have "|- .{`M + 1 ~= `N}. `M := `M + 1 .{`M ~= `N}."
+  also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
     by hoare
   finally show ?thesis .
 qed
 
-lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
   by hoare simp
 
 
@@ -135,24 +135,24 @@
 *}
 
 lemma
-  "|- .{`M = 0 & `S = 0}.
-      WHILE `M ~= a
-      DO `S := `S + b; `M := `M + 1 OD
-      .{`S = a * b}."
+  "|- .{\<acute>M = 0 & \<acute>S = 0}.
+      WHILE \<acute>M ~= a
+      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
+      .{\<acute>S = a * b}."
 proof -
   let "|- _ ?while _" = ?thesis
-  let ".{`?inv}." = ".{`S = `M * b}."
+  let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
 
-  have ".{`M = 0 & `S = 0}. <= .{`?inv}." by auto
-  also have "|- ... ?while .{`?inv & ~ (`M ~= a)}."
+  have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
+  also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
   proof
-    let ?c = "`S := `S + b; `M := `M + 1"
-    have ".{`?inv & `M ~= a}. <= .{`S + b = (`M + 1) * b}."
+    let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
+    have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
       by auto
-    also have "|- ... ?c .{`?inv}." by hoare
-    finally show "|- .{`?inv & `M ~= a}. ?c .{`?inv}." .
+    also have "|- ... ?c .{\<acute>?inv}." by hoare
+    finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
   qed
-  also have "... <= .{`S = a * b}." by auto
+  also have "... <= .{\<acute>S = a * b}." by auto
   finally show ?thesis .
 qed
 
@@ -164,11 +164,11 @@
 *}
 
 lemma
-  "|- .{`M = 0 & `S = 0}.
-      WHILE `M ~= a
-      INV .{`S = `M * b}.
-      DO `S := `S + b; `M := `M + 1 OD
-      .{`S = a * b}."
+  "|- .{\<acute>M = 0 & \<acute>S = 0}.
+      WHILE \<acute>M ~= a
+      INV .{\<acute>S = \<acute>M * b}.
+      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
+      .{\<acute>S = a * b}."
   by hoare auto
 
 
@@ -202,34 +202,34 @@
 
 theorem
   "|- .{True}.
-      `S := 0; `I := 1;
-      WHILE `I ~= n
+      \<acute>S := 0; \<acute>I := 1;
+      WHILE \<acute>I ~= n
       DO
-        `S := `S + `I;
-        `I := `I + 1
+        \<acute>S := \<acute>S + \<acute>I;
+        \<acute>I := \<acute>I + 1
       OD
-      .{`S = (SUM j<n. j)}."
+      .{\<acute>S = (SUM j<n. j)}."
   (is "|- _ (_; ?while) _")
 proof -
   let ?sum = "\<lambda>k. SUM j<k. j"
   let ?inv = "\<lambda>s i. s = ?sum i"
 
-  have "|- .{True}. `S := 0; `I := 1 .{?inv `S `I}."
+  have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
   proof -
     have "True --> 0 = ?sum 1"
       by simp
-    also have "|- .{...}. `S := 0; `I := 1 .{?inv `S `I}."
+    also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
       by hoare
     finally show ?thesis .
   qed
-  also have "|- ... ?while .{?inv `S `I & ~ `I ~= n}."
+  also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
   proof
-    let ?body = "`S := `S + `I; `I := `I + 1"
+    let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
     have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
       by simp
-    also have "|- .{`S + `I = ?sum (`I + 1)}. ?body .{?inv `S `I}."
+    also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
       by hoare
-    finally show "|- .{?inv `S `I & `I ~= n}. ?body .{?inv `S `I}." .
+    finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
   qed
   also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
     by simp
@@ -243,14 +243,14 @@
 
 theorem
   "|- .{True}.
-      `S := 0; `I := 1;
-      WHILE `I ~= n
-      INV .{`S = (SUM j<`I. j)}.
+      \<acute>S := 0; \<acute>I := 1;
+      WHILE \<acute>I ~= n
+      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
       DO
-        `S := `S + `I;
-        `I := `I + 1
+        \<acute>S := \<acute>S + \<acute>I;
+        \<acute>I := \<acute>I + 1
       OD
-      .{`S = (SUM j<n. j)}."
+      .{\<acute>S = (SUM j<n. j)}."
 proof -
   let ?sum = "\<lambda>k. SUM j<k. j"
   let ?inv = "\<lambda>s i. s = ?sum i"
@@ -274,14 +274,14 @@
 
 theorem
   "|- .{True}.
-      `S := 0; `I := 1;
-      WHILE `I ~= n
-      INV .{`S = (SUM j<`I. j)}.
+      \<acute>S := 0; \<acute>I := 1;
+      WHILE \<acute>I ~= n
+      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
       DO
-        `S := `S + `I;
-        `I := `I + 1
+        \<acute>S := \<acute>S + \<acute>I;
+        \<acute>I := \<acute>I + 1
       OD
-      .{`S = (SUM j<n. j)}."
+      .{\<acute>S = (SUM j<n. j)}."
   by hoare auto
 
 end
\ No newline at end of file
diff -r 7d640de604e4 -r 9423817dee84 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Wed Jan 10 00:14:52 2001 +0100
+++ b/src/HOL/ex/Multiquote.thy	Wed Jan 10 00:15:33 2001 +0100
@@ -13,7 +13,7 @@
 
 syntax
   "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"         ("´_" [1000] 1000)
+  "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
 
 parse_translation {*
   let
@@ -35,14 +35,14 @@
 
 text {* basic examples *}
 term ".(a + b + c)."
-term ".(a + b + c + ´x + ´y + 1)."
-term ".(´(f w) + ´x)."
-term ".(f ´x ´y z)."
+term ".(a + b + c + \<acute>x + \<acute>y + 1)."
+term ".(\<acute>(f w) + \<acute>x)."
+term ".(f \<acute>x \<acute>y z)."
 
 text {* advanced examples *}
-term ".(.(´ ´x + ´y).)."
-term ".(.(´ ´x + ´y). o ´f)."
-term ".(´(f o ´g))."
-term ".(.( ´ ´(f o ´g) ).)."
+term ".(.(\<acute>\<acute>x + \<acute>y).)."
+term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
+term ".(\<acute>(f o \<acute>g))."
+term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
 
 end