# HG changeset patch
# User wenzelm
# Date 1301435206 -7200
# Node ID 9bcecd429f7764432210eede13c2aceba98d774b
# Parent  99e359a9db27e97751950c027c26045a40e712c3# Parent  df219e736a5d05c53e7dac48c3e26a85db87849e
merged

diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/CCL.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -85,6 +85,8 @@
 
   apply_def:     "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
   bot_def:         "bot == (lam x. x`x)`(lam x. x`x)"
+
+defs
   fix_def:      "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
 
   (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
@@ -106,6 +108,7 @@
 
   (** Partial Order **)
 
+axioms
   po_refl:        "a [= a"
   po_trans:       "[| a [= b;  b [= c |] ==> a [= c"
   po_cong:        "a [= b ==> f(a) [= f(b)"
@@ -136,6 +139,7 @@
 
   (*** Definitions of Termination and Divergence ***)
 
+defs
   Dvg_def:  "Dvg(t) == t = bot"
   Trm_def:  "Trm(t) == ~ Dvg(t)"
 
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/Fix.thy
--- a/src/CCL/Fix.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Fix.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -9,17 +9,12 @@
 imports Type
 begin
 
-consts
-  idgen      ::       "[i]=>i"
-  INCL      :: "[i=>o]=>o"
+definition idgen :: "i => i"
+  where "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
 
-defs
-  idgen_def:
-  "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
-
-axioms
-  INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
-  po_INCL:    "INCL(%x. a(x) [= b(x))"
+axiomatization INCL :: "[i=>o]=>o" where
+  INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" and
+  po_INCL: "INCL(%x. a(x) [= b(x))" and
   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
 
 
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Hered.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -15,18 +15,13 @@
   is.  Not so useful for functions!
 *}
 
-consts
-      (*** Predicates ***)
-  HTTgen     ::       "i set => i set"
-  HTT        ::       "i set"
+definition HTTgen :: "i set => i set" where
+  "HTTgen(R) ==
+    {t. t=true | t=false | (EX a b. t= <a, b> & a : R & b : R) |
+      (EX f. t = lam x. f(x) & (ALL x. f(x) : R))}"
 
-axioms
-  (*** Definitions of Hereditary Termination ***)
-
-  HTTgen_def:
-  "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b>      & a : R & b : R) |
-                                      (EX f.  t=lam x. f(x) & (ALL x. f(x) : R))}"
-  HTT_def:       "HTT == gfp(HTTgen)"
+definition HTT :: "i set"
+  where "HTT == gfp(HTTgen)"
 
 
 subsection {* Hereditary Termination *}
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Set.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -46,9 +46,9 @@
   "ALL x:A. P"  == "CONST Ball(A, %x. P)"
   "EX x:A. P"   == "CONST Bex(A, %x. P)"
 
-axioms
-  mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
-  set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
+axiomatization where
+  mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" and
+  set_extension: "A = B <-> (ALL x. x:A <-> x:B)"
 
 defs
   Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Term.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -111,8 +111,7 @@
 consts
   napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
 
-axioms
-
+defs
   one_def:                    "one == true"
   if_def:     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
   inl_def:                 "inl(a) == <true,a>"
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Trancl.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -9,21 +9,20 @@
 imports CCL
 begin
 
-consts
-  trans   :: "i set => o"                   (*transitivity predicate*)
-  id      :: "i set"
-  rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
-  trancl  :: "i set => i set"               ("(_^+)" [100] 100)
-  relcomp :: "[i set,i set] => i set"       (infixr "O" 60)
+definition trans :: "i set => o"  (*transitivity predicate*)
+  where "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+
+definition id :: "i set"  (*the identity relation*)
+  where "id == {p. EX x. p = <x,x>}"
 
-axioms
-  trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
-  relcomp_def:     (*composition of relations*)
-                   "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
-  id_def:          (*the identity relation*)
-                   "id == {p. EX x. p = <x,x>}"
-  rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"
-  trancl_def:      "r^+ == r O rtrancl(r)"
+definition relcomp :: "[i set,i set] => i set"  (infixr "O" 60)  (*composition of relations*)
+  where "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+
+definition rtrancl :: "i set => i set"  ("(_^*)" [100] 100)
+  where "r^* == lfp(%s. id Un (r O s))"
+
+definition trancl :: "i set => i set"  ("(_^+)" [100] 100)
+  where "r^+ == r O rtrancl(r)"
 
 
 subsection {* Natural deduction for @{text "trans(r)"} *}
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Type.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -50,7 +50,7 @@
   (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
 *}
 
-axioms
+defs
   Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
   Unit_def:          "Unit == {x. x=one}"
   Bool_def:          "Bool == {x. x=true | x=false}"
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/Flag.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -10,24 +10,24 @@
 imports List
 begin
 
-consts
-  Colour             :: "i set"
-  red                :: "i"
-  white              :: "i"
-  blue               :: "i"
-  ccase              :: "[i,i,i,i]=>i"
-  flag               :: "i"
+definition Colour :: "i set"
+  where "Colour == Unit + Unit + Unit"
+
+definition red :: "i"
+  where "red == inl(one)"
+
+definition white :: "i"
+  where "white == inr(inl(one))"
 
-axioms
+definition blue :: "i"
+  where "blue == inr(inr(one))"
 
-  Colour_def:  "Colour == Unit + Unit + Unit"
-  red_def:        "red == inl(one)"
-  white_def:    "white == inr(inl(one))"
-  blue_def:     "blue == inr(inr(one))"
+definition ccase :: "[i,i,i,i]=>i"
+  where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
 
-  ccase_def:   "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
-
-  flag_def:    "flag == lam l. letrec
+definition flag :: "i"
+  where
+    "flag == lam l. letrec
       flagx l be lcase(l,<[],<[],[]>>,
                        %h t. split(flagx(t),%lr p. split(p,%lw lb.
                             ccase(h, <red$lr,<lw,lb>>,
@@ -35,13 +35,14 @@
                                      <lr,<lw,blue$lb>>))))
       in flagx(l)"
 
-  Flag_def:
-     "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
-                    x = <lr,<lw,lb>> -->
-                  (ALL c:Colour.(c mem lr = true --> c=red) &
-                                (c mem lw = true --> c=white) &
-                                (c mem lb = true --> c=blue)) &
-                  Perm(l,lr @ lw @ lb)"
+axiomatization Perm :: "i => i => o"
+definition Flag :: "i => i => o" where
+  "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
+                x = <lr,<lw,lb>> -->
+              (ALL c:Colour.(c mem lr = true --> c=red) &
+                            (c mem lw = true --> c=white) &
+                            (c mem lb = true --> c=blue)) &
+              Perm(l,lr @ lw @ lb)"
 
 
 lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def
@@ -68,7 +69,7 @@
   apply assumption
   done
 
-lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
+lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}"
   apply (unfold flag_def)
   apply (tactic {* gen_ccs_tac @{context}
     [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/List.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -9,46 +9,47 @@
 imports Nat
 begin
 
-consts
-  map       :: "[i=>i,i]=>i"
-  comp      :: "[i=>i,i=>i]=>i=>i"    (infixr "o" 55)
-  append    :: "[i,i]=>i"             (infixr "@" 55)
-  member    :: "[i,i]=>i"             (infixr "mem" 55)
-  filter    :: "[i,i]=>i"
-  flat      :: "i=>i"
-  partition :: "[i,i]=>i"
-  insert    :: "[i,i,i]=>i"
-  isort     :: "i=>i"
-  qsort     :: "i=>i"
+definition map :: "[i=>i,i]=>i"
+  where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
+
+definition comp :: "[i=>i,i=>i]=>i=>i"  (infixr "\<circ>" 55)
+  where "f \<circ> g == (%x. f(g(x)))"
+
+definition append :: "[i,i]=>i"  (infixr "@" 55)
+  where "l @ m == lrec(l,m,%x xs g. x$g)"
 
-axioms
+axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
+  where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
 
-  map_def:     "map(f,l)   == lrec(l,[],%x xs g. f(x)$g)"
-  comp_def:    "f o g == (%x. f(g(x)))"
-  append_def:  "l @ m == lrec(l,m,%x xs g. x$g)"
-  member_def:  "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
-  filter_def:  "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
-  flat_def:    "flat(l) == lrec(l,[],%h t g. h @ g)"
+definition filter :: "[i,i]=>i"
+  where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
 
-  insert_def:  "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
-  isort_def:   "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+definition flat :: "i=>i"
+  where "flat(l) == lrec(l,[],%h t g. h @ g)"
 
-  partition_def:
+definition partition :: "[i,i]=>i" where
   "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
                             if f`x then part(xs,x$a,b) else part(xs,a,x$b))
                     in part(l,[],[])"
-  qsort_def:   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
+
+definition insert :: "[i,i,i]=>i"
+  where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+
+definition isort :: "i=>i"
+  where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+
+definition qsort :: "i=>i" where
+  "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
                                    let p be partition(f`h,t)
                                    in split(p,%x y. qsortx(x) @ h$qsortx(y)))
                           in qsortx(l)"
 
-
 lemmas list_defs = map_def comp_def append_def filter_def flat_def
   insert_def isort_def partition_def qsort_def
 
 lemma listBs [simp]:
-  "!!f g. (f o g) = (%a. f(g(a)))"
-  "!!a f g. (f o g)(a) = f(g(a))"
+  "!!f g. (f \<circ> g) = (%a. f(g(a)))"
+  "!!a f g. (f \<circ> g)(a) = f(g(a))"
   "!!f. map(f,[]) = []"
   "!!f x xs. map(f,x$xs) = f(x)$map(f,xs)"
   "!!m. [] @ m = m"
@@ -85,7 +86,7 @@
 
 lemma appendTS:
   "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"
-  by (blast intro!: SubtypeI appendT elim!: SubtypeE)
+  by (blast intro!: appendT)
 
 lemma filterT: "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)"
   apply (unfold filter_def)
@@ -105,7 +106,7 @@
 lemma insertTS:
   "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==>  
    insert(f,a,l)  : {x:List(A). P(x)}"
-  by (blast intro!: SubtypeI insertT elim!: SubtypeE)
+  by (blast intro!: insertT)
 
 lemma partitionT:
   "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)"
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/ex/Nat.thy
--- a/src/CCL/ex/Nat.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/Nat.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -9,37 +9,44 @@
 imports Wfd
 begin
 
-consts
+definition not :: "i=>i"
+  where "not(b) == if b then false else true"
+
+definition add :: "[i,i]=>i"  (infixr "#+" 60)
+  where "a #+ b == nrec(a,b,%x g. succ(g))"
 
-  not   :: "i=>i"
-  add   :: "[i,i]=>i"            (infixr "#+" 60)
-  mult  :: "[i,i]=>i"            (infixr "#*" 60)
-  sub   :: "[i,i]=>i"            (infixr "#-" 60)
-  div   :: "[i,i]=>i"            (infixr "##" 60)
-  lt    :: "[i,i]=>i"            (infixr "#<" 60)
-  le    :: "[i,i]=>i"            (infixr "#<=" 60)
-  ackermann :: "[i,i]=>i"
+definition mult :: "[i,i]=>i"  (infixr "#*" 60)
+  where "a #* b == nrec(a,zero,%x g. b #+ g)"
 
-defs
-
-  not_def:     "not(b) == if b then false else true"
+definition sub :: "[i,i]=>i"  (infixr "#-" 60)
+  where
+    "a #- b ==
+      letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
+      in sub(a,b)"
 
-  add_def:     "a #+ b == nrec(a,b,%x g. succ(g))"
-  mult_def:    "a #* b == nrec(a,zero,%x g. b #+ g)"
-  sub_def:     "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
-                        in sub(a,b)"
-  le_def:     "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
-                        in le(a,b)"
-  lt_def:     "a #< b == not(b #<= a)"
+definition le :: "[i,i]=>i"  (infixr "#<=" 60)
+  where
+    "a #<= b ==
+      letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
+      in le(a,b)"
+
+definition lt :: "[i,i]=>i"  (infixr "#<" 60)
+  where "a #< b == not(b #<= a)"
 
-  div_def:    "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y))
-                       in div(a,b)"
-  ack_def:
-  "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.
-                          ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
-                    in ack(a,b)"
+definition div :: "[i,i]=>i"  (infixr "##" 60)
+  where
+    "a ## b ==
+      letrec div x y be if x #< y then zero else succ(div(x#-y,y))
+      in div(a,b)"
 
-lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def
+definition ackermann :: "[i,i]=>i"
+  where
+    "ackermann(a,b) ==
+      letrec ack n m be ncase(n,succ(m),%x.
+        ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
+      in ack(a,b)"
+
+lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def
 
 lemma natBs [simp]:
   "not(true) = false"
@@ -94,7 +101,7 @@
 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
 
 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
-  apply (unfold ack_def)
+  apply (unfold ackermann_def)
   apply (tactic {* gen_ccs_tac @{context} [] 1 *})
   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   done
diff -r 99e359a9db27 -r 9bcecd429f77 src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/Stream.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -9,15 +9,11 @@
 imports List
 begin
 
-consts
-  iter1   ::  "[i=>i,i]=>i"
-  iter2   ::  "[i=>i,i]=>i"
+definition iter1 :: "[i=>i,i]=>i"
+  where "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
 
-defs
-
-  iter1_def:   "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
-  iter2_def:   "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
-
+definition iter2 :: "[i=>i,i]=>i"
+  where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
 
 (*
 Proving properties about infinite lists using coinduction:
@@ -30,9 +26,9 @@
 
 lemma map_comp:
   assumes 1: "l:Lists(A)"
-  shows "map(f o g,l) = map(f,map(g,l))"
+  shows "map(f \<circ> g,l) = map(f,map(g,l))"
   apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
+    "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}" 1 *})
    apply (blast intro: 1)
   apply safe
   apply (drule ListsXH [THEN iffD1])
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/Examples.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -90,7 +90,7 @@
  {c = A^B}"
 apply vcg_simp
 apply(case_tac "b")
- apply(simp add: mod_less)
+ apply simp
 apply simp
 done
 
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/Hoare/ExamplesAbort.thy
--- a/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -14,8 +14,7 @@
 lemma
  "VARS a i j
  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
-apply vcg_simp
-done
+by vcg_simp
 
 lemma "VARS (a::int list) i
  {True}
@@ -24,7 +23,6 @@
  INV {i <= length a}
  DO a[i] := 7; i := i+1 OD
  {True}"
-apply vcg_simp
-done
+by vcg_simp
 
 end
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -10,7 +10,7 @@
 
 theory Hoare_Logic
 imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
 begin
 
 types
@@ -45,11 +45,8 @@
   where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
 
 
-
-(** parse translations **)
-
 syntax
-  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
+  "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
 syntax
  "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
@@ -57,147 +54,11 @@
 syntax ("" output)
  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
-ML {*
-
-local
-
-fun abs((a,T),body) =
-  let val a = absfree(a, dummyT, body)
-  in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
-in
-
-fun mk_abstuple [x] body = abs (x, body)
-  | mk_abstuple (x::xs) body =
-      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
-
-fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
-  | mk_fbody a e ((b,_)::xs) =
-      Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
-
-fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
-end
-*}
-
-(* bexp_tr & assn_tr *)
-(*all meta-variables for bexp except for TRUE are translated as if they
-  were boolean expressions*)
-ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
-  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
-fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-*}
-(* com_tr *)
-ML{*
-fun com_tr (t as (Const(@{syntax_const "_assign"},_) $ x $ e)) xs =
-      (case Syntax.strip_positions x of
-        Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
-      | _ => t)
-  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
-  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
-      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
-      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
-      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
-  | com_tr t _ = t (* if t is just a Free/Var *)
-*}
-
-(* triple_tr *)    (* FIXME does not handle "_idtdummy" *)
-ML{*
-local
-
-fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
-  | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
-      var_tr (Syntax.strip_positions idt) :: vars_tr vars
-  | vars_tr t = [var_tr (Syntax.strip_positions t)]
-
-in
-fun hoare_vars_tr [vars, pre, prg, post] =
-      let val xs = vars_tr vars
-      in Syntax.const @{const_syntax Valid} $
-         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
-      end
-  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-end
-*}
-
-parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
-
 
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
-                            subst_bound (Syntax.free v, dest_abstuple body)
-  | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
-  | dest_abstuple trm = trm;
-
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
-  | abs2list (Abs(x,T,t)) = [Free (x, T)]
-  | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
-  | mk_ts (Abs(x,_,t)) = mk_ts t
-  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
-  | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
-           ((Syntax.free x)::(abs2list t), mk_ts t)
-  | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
-  | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
-  | find_ch ((v,t)::vts) i xs =
-      if t = Bound i then find_ch vts (i-1) xs
-      else (true, (v, subst_bounds (xs, t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
-  | is_f (Abs(x,_,t)) = true
-  | is_f t = false;
-*}
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
 
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_syntax inter}, _) $
-        (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
-      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
-  | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
-  let val (vs, ts) = mk_vts f;
-      val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in
-    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
-    else Syntax.const @{const_syntax annskip}
-  end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
-      if is_f f then mk_assign f
-      else Syntax.const @{const_syntax Basic} $ f
-  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
-      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
-      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
-      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
-  | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
-  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -7,7 +7,7 @@
 
 theory Hoare_Logic_Abort
 imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
 begin
 
 types
@@ -47,11 +47,8 @@
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
 
 
-
-(** parse translations **)
-
 syntax
-  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
+  "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
 syntax
   "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
@@ -59,146 +56,12 @@
 syntax ("" output)
   "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
-ML {*
-
-local
-fun free a = Free(a,dummyT)
-fun abs((a,T),body) =
-  let val a = absfree(a, dummyT, body)
-  in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
-in
-
-fun mk_abstuple [x] body = abs (x, body)
-  | mk_abstuple (x::xs) body =
-      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
-
-fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
-  | mk_fbody a e ((b,_)::xs) =
-      Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs;
-
-fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
-end
-*}
-
-(* bexp_tr & assn_tr *)
-(*all meta-variables for bexp except for TRUE are translated as if they
-  were boolean expressions*)
-ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
-  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
-fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-*}
-(* com_tr *)
-ML{*
-fun com_tr (t as (Const (@{syntax_const "_assign"},_) $ x $ e)) xs =
-      (case Syntax.strip_positions x of
-        Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
-      | _ => t)
-  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
-  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
-      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
-      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
-      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
-  | com_tr t _ = t (* if t is just a Free/Var *)
-*}
-
-(* triple_tr *)    (* FIXME does not handle "_idtdummy" *)
-ML{*
-local
-
-fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
-  | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
-      var_tr (Syntax.strip_positions idt) :: vars_tr vars
-  | vars_tr t = [var_tr (Syntax.strip_positions t)]
-
-in
-fun hoare_vars_tr [vars, pre, prg, post] =
-      let val xs = vars_tr vars
-      in Syntax.const @{const_syntax Valid} $
-         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
-      end
-  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-end
-*}
-
-parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, hoare_vars_tr)] *}
-
 
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
-      subst_bound (Syntax.free v, dest_abstuple body)
-  | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
-  | dest_abstuple trm = trm;
-
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
-  | abs2list (Abs(x,T,t)) = [Free (x, T)]
-  | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
-  | mk_ts (Abs(x,_,t)) = mk_ts t
-  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
-  | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
-           ((Syntax.free x)::(abs2list t), mk_ts t)
-  | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
-  | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
-  | find_ch ((v,t)::vts) i xs =
-      if t = Bound i then find_ch vts (i-1) xs
-      else (true, (v, subst_bounds (xs,t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
-  | is_f (Abs(x,_,t)) = true
-  | is_f t = false;
-*}
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation
+  {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
 
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
-        (Const (@{const_syntax Collect},_) $ T2)) =
-      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
-  | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
-  | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
-  let val (vs, ts) = mk_vts f;
-      val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in
-    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
-    else Syntax.const @{const_syntax annskip}
-  end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
-      if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
-  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
-      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
-      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
-      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
-  | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
-  Syntax.const @{syntax_const "_hoare_abort"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 (*** The proof rules ***)
 
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Tue Mar 29 23:46:46 2011 +0200
@@ -40,7 +40,7 @@
 done
 
 lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
-apply (clarsimp simp only:Image_iff intro:subsetI)
+apply (clarsimp simp only:Image_iff)
 apply (erule rtrancl_induct)
  apply blast
 apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/Hoare/hoare_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML	Tue Mar 29 23:46:46 2011 +0200
@@ -0,0 +1,156 @@
+(*  Title:      HOL/Hoare/hoare_syntax.ML
+    Author:     Leonor Prensa Nieto & Tobias Nipkow
+
+Syntax translations for Hoare logic.
+*)
+
+signature HOARE_SYNTAX =
+sig
+  val hoare_vars_tr: term list -> term
+  val spec_tr': string -> term list -> term
+end;
+
+structure Hoare_Syntax: HOARE_SYNTAX =
+struct
+
+(** parse translation **)
+
+local
+
+fun idt_name (Free (x, _)) = SOME x
+  | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
+  | idt_name _ = NONE;
+
+fun eq_idt tu =
+  (case pairself idt_name tu of
+    (SOME x, SOME y) => x = y
+  | _ => false);
+
+fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
+  | mk_abstuple (x :: xs) body =
+      Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
+
+fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
+  | mk_fbody x e (y :: xs) =
+      Syntax.const @{const_syntax Pair} $
+        (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
+
+fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
+
+
+(* bexp_tr & assn_tr *)
+(*all meta-variables for bexp except for TRUE are translated as if they
+  were boolean expressions*)
+
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
+  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
+
+
+(* com_tr *)
+
+fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
+      Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
+  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+  | com_tr t _ = t;
+
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
+  | vars_tr t = [t];
+
+in
+
+fun hoare_vars_tr [vars, pre, prg, post] =
+      let val xs = vars_tr vars
+      in Syntax.const @{const_syntax Valid} $
+         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+      end
+  | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+
+end;
+
+
+
+(** print translation **)
+
+local
+
+fun dest_abstuple
+      (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
+        subst_bound (Syntax.free v, dest_abstuple body)
+  | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
+  | dest_abstuple tm = tm;
+
+fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+  | abs2list (Abs (x, T, t)) = [Free (x, T)]
+  | abs2list _ = [];
+
+fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
+  | mk_ts (Abs (x, _, t)) = mk_ts t
+  | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
+  | mk_ts t = [t];
+
+fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
+      (Syntax.free x :: abs2list t, mk_ts t)
+  | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
+  | mk_vts t = raise Match;
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
+  | find_ch ((v, t) :: vts) i xs =
+      if t = Bound i then find_ch vts (i - 1) xs
+      else (true, (v, subst_bounds (xs, t)));
+
+fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
+  | is_f (Abs (x, _, t)) = true
+  | is_f t = false;
+
+
+(* assn_tr' & bexp_tr'*)
+
+fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+  | assn_tr' (Const (@{const_syntax inter}, _) $
+        (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) =
+      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
+  | assn_tr' t = t;
+
+fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+  | bexp_tr' t = t;
+
+
+(* com_tr' *)
+
+fun mk_assign f =
+  let
+    val (vs, ts) = mk_vts f;
+    val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
+  in
+    if ch
+    then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+    else Syntax.const @{const_syntax annskip}
+  end;
+
+fun com_tr' (Const (@{const_syntax Basic}, _) $ f) =
+      if is_f f then mk_assign f
+      else Syntax.const @{const_syntax Basic} $ f
+  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) =
+      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) =
+      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
+  | com_tr' t = t;
+
+in
+
+fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
+
+end;
+
+end;
+
diff -r 99e359a9db27 -r 9bcecd429f77 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue Mar 29 23:46:46 2011 +0200
@@ -650,12 +650,12 @@
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
 
 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy	\
-  Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy			\
-  Hoare/Hoare_Logic.thy	Hoare/Hoare_Logic_Abort.thy			\
+  Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML		\
+  Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy	\
   Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML		\
   Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
-  Hoare/SchorrWaite.thy Hoare/Separation.thy				\
-  Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
+  Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy	\
+  Hoare/document/root.tex Hoare/document/root.bib
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
 
 
diff -r 99e359a9db27 -r 9bcecd429f77 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 29 22:06:53 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 29 23:46:46 2011 +0200
@@ -36,6 +36,7 @@
   val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term
   val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
   val constrainAbsC: string
+  val abs_tr: term list -> term
   val pure_trfuns:
     (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
@@ -97,7 +98,6 @@
 fun idtypdummy_ast_tr (*"_idtypdummy"*) [ty] =
       Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
   | idtypdummy_ast_tr (*"_idtypdummy"*) asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
 fun lambda_ast_tr (*"_lambda"*) [pats, body] =
       Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
   | lambda_ast_tr (*"_lambda"*) asts = raise Ast.AST ("lambda_ast_tr", asts);