# HG changeset patch
# User wenzelm
# Date 1452625553 -3600
# Node ID ec2f0dad8b98b98ddaf77e0b62d9d8e3755f157f
# Parent  18a217591310e0b395b62b2c36ed2ac99e2413a4# Parent  b855771b39798fa3a5b0b88a82eeabc87e184e36
merged

diff -r 18a217591310 -r ec2f0dad8b98 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/CCL.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -320,17 +320,17 @@
   apply blast
   done
 
-lemma POgenXH: 
-  "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |  
-           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |  
+lemma POgenXH:
+  "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
+           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
            (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))"
   apply (unfold POgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
-lemma poXH: 
-  "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |  
-                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |  
+lemma poXH:
+  "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))"
   apply (simp add: PO_iff del: ex_simps)
   apply (rule POgen_mono
@@ -438,18 +438,18 @@
   apply blast
   done
 
-lemma EQgenXH: 
-  "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |  
-                                             (t=false \<and> t'=false) |  
-                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |  
+lemma EQgenXH:
+  "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |
+                                             (t=false \<and> t'=false) |
+                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
   apply (unfold EQgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
-lemma eqXH: 
-  "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |  
-                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |  
+lemma eqXH:
+  "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
+                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |
                      (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
   apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
     (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
diff -r 18a217591310 -r ec2f0dad8b98 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/Set.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -9,62 +9,18 @@
 typedecl 'a set
 instance set :: ("term") "term" ..
 
-consts
-  Collect       :: "['a \<Rightarrow> o] \<Rightarrow> 'a set"                    (*comprehension*)
-  Compl         :: "('a set) \<Rightarrow> 'a set"                     (*complement*)
-  Int           :: "['a set, 'a set] \<Rightarrow> 'a set"         (infixl "Int" 70)
-  Un            :: "['a set, 'a set] \<Rightarrow> 'a set"         (infixl "Un" 65)
-  Union         :: "(('a set)set) \<Rightarrow> 'a set"                (*...of a set*)
-  Inter         :: "(('a set)set) \<Rightarrow> 'a set"                (*...of a set*)
-  UNION         :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"       (*general*)
-  INTER         :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"       (*general*)
-  Ball          :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"                 (*bounded quants*)
-  Bex           :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"                 (*bounded quants*)
-  mono          :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"                (*monotonicity*)
-  mem           :: "['a, 'a set] \<Rightarrow> o"                  (infixl ":" 50) (*membership*)
-  subset        :: "['a set, 'a set] \<Rightarrow> o"              (infixl "<=" 50)
-  singleton     :: "'a \<Rightarrow> 'a set"                       ("{_}")
-  empty         :: "'a set"                             ("{}")
+
+subsection \<open>Set comprehension and membership\<close>
+
+axiomatization Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set"
+  and mem :: "['a, 'a set] \<Rightarrow> o"  (infixl ":" 50)
+where mem_Collect_iff: "(a : Collect(P)) \<longleftrightarrow> P(a)"
+  and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
 
 syntax
-  "_Coll"       :: "[idt, o] \<Rightarrow> 'a set"                 ("(1{_./ _})") (*collection*)
-
-  (* Big Intersection / Union *)
-
-  "_INTER"      :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
-  "_UNION"      :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
-
-  (* Bounded Quantifiers *)
-
-  "_Ball"       :: "[idt, 'a set, o] \<Rightarrow> o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
-  "_Bex"        :: "[idt, 'a set, o] \<Rightarrow> o"              ("(EX _:_./ _)" [0, 0, 0] 10)
-
+  "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  ("(1{_./ _})")
 translations
-  "{x. P}"      == "CONST Collect(\<lambda>x. P)"
-  "INT x:A. B"  == "CONST INTER(A, \<lambda>x. B)"
-  "UN x:A. B"   == "CONST UNION(A, \<lambda>x. B)"
-  "ALL x:A. P"  == "CONST Ball(A, \<lambda>x. P)"
-  "EX x:A. P"   == "CONST Bex(A, \<lambda>x. P)"
-
-axiomatization where
-  mem_Collect_iff: "(a : {x. P(x)}) \<longleftrightarrow> P(a)" and
-  set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
-
-defs
-  Ball_def:      "Ball(A, P)  == ALL x. x:A \<longrightarrow> P(x)"
-  Bex_def:       "Bex(A, P)   == EX x. x:A \<and> P(x)"
-  mono_def:      "mono(f)     == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
-  subset_def:    "A <= B      == ALL x:A. x:B"
-  singleton_def: "{a}         == {x. x=a}"
-  empty_def:     "{}          == {x. False}"
-  Un_def:        "A Un B      == {x. x:A | x:B}"
-  Int_def:       "A Int B     == {x. x:A \<and> x:B}"
-  Compl_def:     "Compl(A)    == {x. \<not>x:A}"
-  INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
-  UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
-  Inter_def:     "Inter(S)    == (INT x:S. x)"
-  Union_def:     "Union(S)    == (UN x:S. x)"
-
+  "{x. P}" == "CONST Collect(\<lambda>x. P)"
 
 lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
   apply (rule mem_Collect_iff [THEN iffD2])
@@ -85,6 +41,19 @@
 
 subsection \<open>Bounded quantifiers\<close>
 
+definition Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"
+  where "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)"
+
+definition Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"
+  where "Bex(A, P) == EX x. x:A \<and> P(x)"
+
+syntax
+  "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(ALL _:_./ _)" [0, 0, 0] 10)
+  "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(EX _:_./ _)" [0, 0, 0] 10)
+translations
+  "ALL x:A. P"  == "CONST Ball(A, \<lambda>x. P)"
+  "EX x:A. P"   == "CONST Bex(A, \<lambda>x. P)"
+
 lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
   by (simp add: Ball_def)
 
@@ -107,8 +76,7 @@
 lemma ball_rew: "(ALL x:A. True) \<longleftrightarrow> True"
   by (blast intro: ballI)
 
-
-subsection \<open>Congruence rules\<close>
+subsubsection \<open>Congruence rules\<close>
 
 lemma ball_cong:
   "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow>
@@ -121,6 +89,52 @@
   by (blast intro: bexI elim: bexE)
 
 
+subsection \<open>Further operations\<close>
+
+definition subset :: "['a set, 'a set] \<Rightarrow> o"  (infixl "<=" 50)
+  where "A <= B == ALL x:A. x:B"
+
+definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"
+  where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
+
+definition singleton :: "'a \<Rightarrow> 'a set"  ("{_}")
+  where "{a} == {x. x=a}"
+
+definition empty :: "'a set"  ("{}")
+  where "{} == {x. False}"
+
+definition Un :: "['a set, 'a set] \<Rightarrow> 'a set"  (infixl "Un" 65)
+  where "A Un B == {x. x:A | x:B}"
+
+definition Int :: "['a set, 'a set] \<Rightarrow> 'a set"  (infixl "Int" 70)
+  where "A Int B == {x. x:A \<and> x:B}"
+
+definition Compl :: "('a set) \<Rightarrow> 'a set"
+  where "Compl(A) == {x. \<not>x:A}"
+
+
+subsection \<open>Big Intersection / Union\<close>
+
+definition INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"
+  where "INTER(A, B) == {y. ALL x:A. y: B(x)}"
+
+definition UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"
+  where "UNION(A, B) == {y. EX x:A. y: B(x)}"
+
+syntax
+  "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(INT _:_./ _)" [0, 0, 0] 10)
+  "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(UN _:_./ _)" [0, 0, 0] 10)
+translations
+  "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
+  "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
+
+definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
+  where "Inter(S) == (INT x:S. x)"
+
+definition Union :: "(('a set)set) \<Rightarrow> 'a set"
+  where "Union(S) == (UN x:S. x)"
+
+
 subsection \<open>Rules for subsets\<close>
 
 lemma subsetI: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B"
diff -r 18a217591310 -r ec2f0dad8b98 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/Term.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -9,48 +9,69 @@
 imports CCL
 begin
 
-consts
+definition one :: "i"
+  where "one == true"
 
-  one        :: "i"
+definition "if" :: "[i,i,i]\<Rightarrow>i"  ("(3if _/ then _/ else _)" [0,0,60] 60)
+  where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
-  "if"       :: "[i,i,i]\<Rightarrow>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
+definition inl :: "i\<Rightarrow>i"
+  where "inl(a) == <true,a>"
 
-  inl        :: "i\<Rightarrow>i"
-  inr        :: "i\<Rightarrow>i"
-  "when"     :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+definition inr :: "i\<Rightarrow>i"
+  where "inr(b) == <false,b>"
+
+definition split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
 
-  split      :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
-  fst        :: "i\<Rightarrow>i"
-  snd        :: "i\<Rightarrow>i"
-  thd        :: "i\<Rightarrow>i"
+definition "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
+
+definition fst :: "i\<Rightarrow>i"
+  where "fst(t) == split(t, \<lambda>x y. x)"
 
-  zero       :: "i"
-  succ       :: "i\<Rightarrow>i"
-  ncase      :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
-  nrec       :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition snd :: "i\<Rightarrow>i"
+  where "snd(t) == split(t, \<lambda>x y. y)"
+
+definition thd :: "i\<Rightarrow>i"
+  where "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
+
+definition zero :: "i"
+  where "zero == inl(one)"
 
-  nil        :: "i"                        ("([])")
-  cons       :: "[i,i]\<Rightarrow>i"                 (infixr "$" 80)
-  lcase      :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
-  lrec       :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition succ :: "i\<Rightarrow>i"
+  where "succ(n) == inr(n)"
+
+definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
 
-  "let"      :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
-  letrec     :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  letrec2    :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  letrec3    :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+
+no_syntax
+  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+
+definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
 syntax
-  "_let"     :: "[id,i,i]\<Rightarrow>i"             ("(3let _ be _/ in _)"
-                        [0,0,60] 60)
+  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
 
-  "_letrec"  :: "[id,id,i,i]\<Rightarrow>i"         ("(3letrec _ _ be _/ in _)"
-                        [0,0,0,60] 60)
+definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+
+definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec2 (h, f) ==
+    letrec (\<lambda>p g'. split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>))), \<lambda>g'. f(\<lambda>x y. g'(<x,y>)))"
 
-  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"     ("(3letrec _ _ _ be _/ in _)"
-                        [0,0,0,0,60] 60)
+definition letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec3 (h, f) ==
+    letrec (\<lambda>p g'. split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>)))),
+      \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
-  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)"
-                        [0,0,0,0,0,60] 60)
+syntax
+  "_let" :: "[id,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+  "_letrec" :: "[id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
 
 ML \<open>
 (** Quantifier translations: variable binding **)
@@ -107,42 +128,24 @@
   (@{const_syntax letrec3}, K letrec3_tr')]
 \<close>
 
-consts
-  napply     :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
+
+definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
+
+definition nil :: "i"  ("([])")
+  where "[] == inl(one)"
 
-defs
-  one_def:                    "one == true"
-  if_def:     "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
-  inl_def:                 "inl(a) == <true,a>"
-  inr_def:                 "inr(b) == <false,b>"
-  when_def:           "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
-  split_def:           "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
-  fst_def:                 "fst(t) == split(t, \<lambda>x y. x)"
-  snd_def:                 "snd(t) == split(t, \<lambda>x y. y)"
-  thd_def:                 "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
-  zero_def:                  "zero == inl(one)"
-  succ_def:               "succ(n) == inr(n)"
-  ncase_def:         "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
-  nrec_def:          " nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
-  nil_def:                     "[] == inl(one)"
-  cons_def:                   "h$t == inr(<h,t>)"
-  lcase_def:         "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
-  lrec_def:           "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
+definition cons :: "[i,i]\<Rightarrow>i"  (infixr "$" 80)
+  where "h$t == inr(<h,t>)"
+
+definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
 
-  let_def:  "let x be t in f(x) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-  letrec_def:
-  "letrec g x be h(x,g) in b(g) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
-  letrec2_def:  "letrec g x y be h(x,y,g) in f(g)==
-               letrec g' p be split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>)))
-                          in f(\<lambda>x y. g'(<x,y>))"
-
-  letrec3_def:  "letrec g x y z be h(x,y,z,g) in f(g) ==
-             letrec g' p be split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>))))
-                          in f(\<lambda>x y z. g'(<x,<y,z>>))"
-
-  napply_def: "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
-
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  ("(_ ^ _ ` _)" [56,56,56] 56)
+  where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
   and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
diff -r 18a217591310 -r ec2f0dad8b98 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/Type.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -9,42 +9,39 @@
 imports Term
 begin
 
-consts
-
-  Subtype       :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set"
-  Bool          :: "i set"
-  Unit          :: "i set"
-  Plus           :: "[i set, i set] \<Rightarrow> i set"        (infixr "+" 55)
-  Pi            :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
-  Sigma         :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
-  Nat           :: "i set"
-  List          :: "i set \<Rightarrow> i set"
-  Lists         :: "i set \<Rightarrow> i set"
-  ILists        :: "i set \<Rightarrow> i set"
-  TAll          :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"       (binder "TALL " 55)
-  TEx           :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"       (binder "TEX " 55)
-  Lift          :: "i set \<Rightarrow> i set"                  ("(3[_])")
-
-  SPLIT         :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
+definition Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set"
+  where "Subtype(A, P) == {x. x:A \<and> P(x)}"
 
 syntax
-  "_Pi"         :: "[idt, i set, i set] \<Rightarrow> i set"    ("(3PROD _:_./ _)"
-                                [0,0,60] 60)
+  "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  ("(1{_: _ ./ _})")
+translations
+  "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
 
-  "_Sigma"      :: "[idt, i set, i set] \<Rightarrow> i set"    ("(3SUM _:_./ _)"
-                                [0,0,60] 60)
+definition Unit :: "i set"
+  where "Unit == {x. x=one}"
+
+definition Bool :: "i set"
+  where "Bool == {x. x=true | x=false}"
+
+definition Plus :: "[i set, i set] \<Rightarrow> i set"  (infixr "+" 55)
+  where "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
 
-  "_arrow"      :: "[i set, i set] \<Rightarrow> i set"         ("(_ ->/ _)"  [54, 53] 53)
-  "_star"       :: "[i set, i set] \<Rightarrow> i set"         ("(_ */ _)" [56, 55] 55)
-  "_Subtype"    :: "[idt, 'a set, o] \<Rightarrow> 'a set"      ("(1{_: _ ./ _})")
+definition Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+  where "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}"
+
+definition Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+  where "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
 
+syntax
+  "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set"  ("(3PROD _:_./ _)" [0,0,60] 60)
+  "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set"  ("(3SUM _:_./ _)" [0,0,60] 60)
+  "_arrow" :: "[i set, i set] \<Rightarrow> i set"  ("(_ ->/ _)"  [54, 53] 53)
+  "_star"  :: "[i set, i set] \<Rightarrow> i set"  ("(_ */ _)" [56, 55] 55)
 translations
-  "PROD x:A. B" => "CONST Pi(A, \<lambda>x. B)"
-  "A -> B"      => "CONST Pi(A, \<lambda>_. B)"
-  "SUM x:A. B"  => "CONST Sigma(A, \<lambda>x. B)"
-  "A * B"       => "CONST Sigma(A, \<lambda>_. B)"
-  "{x: A. B}"   == "CONST Subtype(A, \<lambda>x. B)"
-
+  "PROD x:A. B" \<rightharpoonup> "CONST Pi(A, \<lambda>x. B)"
+  "A -> B" \<rightharpoonup> "CONST Pi(A, \<lambda>_. B)"
+  "SUM x:A. B" \<rightharpoonup> "CONST Sigma(A, \<lambda>x. B)"
+  "A * B" \<rightharpoonup> "CONST Sigma(A, \<lambda>_. B)"
 print_translation \<open>
  [(@{const_syntax Pi},
     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
@@ -52,28 +49,34 @@
     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
 \<close>
 
-defs
-  Subtype_def: "{x:A. P(x)} == {x. x:A \<and> P(x)}"
-  Unit_def:          "Unit == {x. x=one}"
-  Bool_def:          "Bool == {x. x=true | x=false}"
-  Plus_def:           "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
-  Pi_def:         "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}"
-  Sigma_def:   "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
-  Nat_def:            "Nat == lfp(\<lambda>X. Unit + X)"
-  List_def:       "List(A) == lfp(\<lambda>X. Unit + A*X)"
+definition Nat :: "i set"
+  where "Nat == lfp(\<lambda>X. Unit + X)"
+
+definition List :: "i set \<Rightarrow> i set"
+  where "List(A) == lfp(\<lambda>X. Unit + A*X)"
+
+definition Lists :: "i set \<Rightarrow> i set"
+  where "Lists(A) == gfp(\<lambda>X. Unit + A*X)"
+
+definition ILists :: "i set \<Rightarrow> i set"
+  where "ILists(A) == gfp(\<lambda>X.{} + A*X)"
 
-  Lists_def:     "Lists(A) == gfp(\<lambda>X. Unit + A*X)"
-  ILists_def:   "ILists(A) == gfp(\<lambda>X.{} + A*X)"
+
+definition TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"  (binder "TALL " 55)
+  where "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
 
-  Tall_def:   "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
-  Tex_def:     "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
-  Lift_def:           "[A] == A Un {bot}"
+definition TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"  (binder "TEX " 55)
+  where "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
 
-  SPLIT_def:   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
+definition Lift :: "i set \<Rightarrow> i set"  ("(3[_])")
+  where "[A] == A Un {bot}"
+
+definition SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
+  where "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
 
 
 lemmas simp_type_defs =
-    Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def
+    Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def TAll_def TEx_def
   and ind_type_defs = Nat_def List_def
   and simp_data_defs = one_def inl_def inr_def
   and ind_data_defs = zero_def succ_def nil_def cons_def
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -948,6 +948,29 @@
 \<close>
 
 
+section \<open>Proof state output \label{sec:state-output}\<close>
+
+text \<open>
+  FIXME
+  \figref{fig:output-and-state} versus \figref{fig:output-including-state}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{output-and-state}
+  \end{center}
+  \caption{Separate proof state display (right) and other output (bottom).}
+  \label{fig:output-and-state}
+  \end{figure}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{output-including-state}
+  \end{center}
+  \caption{Proof state display within the regular output panel}
+  \label{fig:output-including-state}
+  \end{figure}
+\<close>
+
 section \<open>Query \label{sec:query}\<close>
 
 text \<open>
@@ -967,7 +990,7 @@
   \begin{center}
   \includegraphics[scale=0.333]{query}
   \end{center}
-  \caption{An instance of the Query panel}
+  \caption{An instance of the Query panel: find theorems}
   \label{fig:query}
   \end{figure}
 
@@ -1655,6 +1678,22 @@
 \<close>
 
 
+section \<open>Markdown structure\<close>
+
+text \<open>
+  FIXME
+  \figref{fig:markdown-document}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{markdown-document}
+  \end{center}
+  \caption{Markdown structure within document text}
+  \label{fig:markdown-document}
+  \end{figure}
+\<close>
+
+
 section \<open>Citations and Bib{\TeX} entries\<close>
 
 text \<open>
@@ -1694,6 +1733,22 @@
 \<close>
 
 
+chapter \<open>ML debugger\<close>
+
+text \<open>
+  FIXME
+  \figref{fig:ml-debugger}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{ml-debugger}
+  \end{center}
+  \caption{ML debugger}
+  \label{fig:ml-debugger}
+  \end{figure}
+\<close>
+
+
 chapter \<open>Miscellaneous tools\<close>
 
 section \<open>Timing\<close>
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/auto-tools.png
Binary file src/Doc/JEdit/document/auto-tools.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/bibtex-mode.png
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/cite-completion.png
Binary file src/Doc/JEdit/document/cite-completion.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/isabelle-jedit-hdpi.png
Binary file src/Doc/JEdit/document/isabelle-jedit-hdpi.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/isabelle-jedit.png
Binary file src/Doc/JEdit/document/isabelle-jedit.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/markdown-document.png
Binary file src/Doc/JEdit/document/markdown-document.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/ml-debugger.png
Binary file src/Doc/JEdit/document/ml-debugger.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/output-and-state.png
Binary file src/Doc/JEdit/document/output-and-state.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/output-including-state.png
Binary file src/Doc/JEdit/document/output-including-state.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/output.png
Binary file src/Doc/JEdit/document/output.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/popup1.png
Binary file src/Doc/JEdit/document/popup1.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/popup2.png
Binary file src/Doc/JEdit/document/popup2.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/query.png
Binary file src/Doc/JEdit/document/query.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/sidekick-document.png
Binary file src/Doc/JEdit/document/sidekick-document.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/sidekick.png
Binary file src/Doc/JEdit/document/sidekick.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/sledgehammer.png
Binary file src/Doc/JEdit/document/sledgehammer.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/JEdit/document/theories.png
Binary file src/Doc/JEdit/document/theories.png has changed
diff -r 18a217591310 -r ec2f0dad8b98 src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Doc/ROOT	Tue Jan 12 20:05:53 2016 +0100
@@ -207,15 +207,19 @@
     "bibtex-mode.png"
     "build"
     "cite-completion.png"
+    "isabelle-jedit-hdpi.png"
     "isabelle-jedit.png"
-    "isabelle-jedit-hdpi.png"
+    "markdown-document.png"
+    "ml-debugger.png"
+    "output-and-state.png"
+    "output-including-state.png"
     "output.png"
-    "query.png"
     "popup1.png"
     "popup2.png"
+    "query.png"
     "root.tex"
+    "sidekick-document.png"
     "sidekick.png"
-    "sidekick-document.png"
     "sledgehammer.png"
     "theories.png"
 
diff -r 18a217591310 -r ec2f0dad8b98 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/FOLP/IFOLP.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -28,15 +28,12 @@
  eq             ::      "['a,'a] => o"  (infixl "=" 50)
  True           ::      "o"
  False          ::      "o"
- Not            ::      "o => o"        ("~ _" [40] 40)
  conj           ::      "[o,o] => o"    (infixr "&" 35)
  disj           ::      "[o,o] => o"    (infixr "|" 30)
  imp            ::      "[o,o] => o"    (infixr "-->" 25)
- iff            ::      "[o,o] => o"    (infixr "<->" 25)
       (*Quantifiers*)
  All            ::      "('a => o) => o"        (binder "ALL " 10)
  Ex             ::      "('a => o) => o"        (binder "EX " 10)
- Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
       (*Rewriting gadgets*)
  NORM           ::      "o => o"
  norm           ::      "'a => 'a"
@@ -157,12 +154,15 @@
 
 (**** Definitions ****)
 
-defs
-not_def:              "~P == P-->False"
-iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
+definition Not :: "o => o"  ("~ _" [40] 40)
+  where not_def: "~P == P-->False"
+
+definition iff :: "[o,o] => o"  (infixr "<->" 25)
+  where "P<->Q == (P-->Q) & (Q-->P)"
 
 (*Unique existence*)
-ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+definition Ex1 :: "('a => o) => o"  (binder "EX! " 10)
+  where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
 
 (*Rewriting -- special constants to flag normalized terms and formulae*)
 axiomatization where
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/Auth/All_Symmetric.thy
--- a/src/HOL/Auth/All_Symmetric.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Auth/All_Symmetric.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -4,7 +4,10 @@
 
 text \<open>All keys are symmetric\<close>
 
-defs all_symmetric_def: "all_symmetric \<equiv> True"
+overloading all_symmetric \<equiv> all_symmetric
+begin
+  definition "all_symmetric \<equiv> True"
+end
 
 lemma isSym_keys: "K \<in> symKeys"
   by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Bali/Example.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -141,12 +141,16 @@
 lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
+
 subsubsection "classes and interfaces"
 
-defs
-
-  Object_mdecls_def: "Object_mdecls \<equiv> []"
-  SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
+overloading
+  Object_mdecls \<equiv> Object_mdecls
+  SXcpt_mdecls \<equiv> SXcpt_mdecls
+begin
+  definition "Object_mdecls \<equiv> []"
+  definition "SXcpt_mdecls  \<equiv> []"
+end
 
 axiomatization  
   foo    :: mname
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/HOL.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -69,25 +69,38 @@
 
 typedecl bool
 
-judgment
-  Trueprop      :: "bool \<Rightarrow> prop"                   ("(_)" 5)
+judgment Trueprop :: "bool \<Rightarrow> prop"  ("(_)" 5)
+
+axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
+  and eq :: "['a, 'a] \<Rightarrow> bool"  (infixl "=" 50)
+  and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+
 
-axiomatization
-  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<longrightarrow>" 25)  and
-  eq            :: "['a, 'a] \<Rightarrow> bool"               (infixl "=" 50)  and
-  The           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+subsubsection \<open>Defined connectives and quantifiers\<close>
+
+definition True :: bool
+  where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
+
+definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10)
+  where "All P \<equiv> (P = (\<lambda>x. True))"
 
-consts
-  True          :: bool
-  False         :: bool
-  Not           :: "bool \<Rightarrow> bool"                   ("\<not> _" [40] 40)
+definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10)
+  where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
+
+definition False :: bool
+  where "False \<equiv> (\<forall>P. P)"
+
+definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40)
+  where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
-  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<and>" 35)
-  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<or>" 30)
+definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35)
+  where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
 
-  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<forall>" 10)
-  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>" 10)
-  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>!" 10)
+definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
+  where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
+
+definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>!" 10)
+  where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
@@ -167,16 +180,6 @@
   iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
   True_or_False: "(P = True) \<or> (P = False)"
 
-defs
-  True_def:     "True      \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
-  All_def:      "All P     \<equiv> (P = (\<lambda>x. True))"
-  Ex_def:       "Ex P      \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
-  False_def:    "False     \<equiv> (\<forall>P. P)"
-  not_def:      "\<not> P       \<equiv> P \<longrightarrow> False"
-  and_def:      "P \<and> Q     \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
-  or_def:       "P \<or> Q     \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
-  Ex1_def:      "Ex1 P     \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
-
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
   where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -29,8 +29,10 @@
          THEN Loc Res:==(%s. 1)
          ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
 
-defs
-  bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
+overloading bodies \<equiv> bodies
+begin
+  definition "bodies == [(Even,evn),(Odd,odd)]"
+end
 
 definition
   Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/IMPP/Misc.thy
--- a/src/HOL/IMPP/Misc.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IMPP/Misc.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -8,13 +8,29 @@
 imports Hoare
 begin
 
-defs
-  newlocs_def: "newlocs       == %x. undefined"
-  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
-  getlocs_def: "getlocs s     == case s of st g l => l"
-   update_def: "update s vn v == case vn of
-                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
-                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+overloading
+  newlocs \<equiv> newlocs
+  setlocs \<equiv> setlocs
+  getlocs \<equiv> getlocs
+  update \<equiv> update
+begin
+
+definition newlocs :: locals
+  where "newlocs == %x. undefined"
+
+definition setlocs :: "state => locals => state"
+  where "setlocs s l' == case s of st g l => st g l'"
+
+definition getlocs :: "state => locals"
+  where "getlocs s == case s of st g l => l"
+
+definition update  :: "state => vname => val => state"
+  where "update s vn v ==
+    case vn of
+      Glb gn => (case s of st g l => st (g(gn:=v)) l)
+    | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+
+end
 
 
 subsection "state access"
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/IOA/Asig.thy
--- a/src/HOL/IOA/Asig.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IOA/Asig.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -9,41 +9,31 @@
 imports Main
 begin
 
-type_synonym
-  'a signature = "('a set * 'a set * 'a set)"
+type_synonym 'a signature = "('a set * 'a set * 'a set)"
+
+definition "inputs" :: "'action signature => 'action set"
+  where asig_inputs_def: "inputs == fst"
 
-consts
-  "actions" :: "'action signature => 'action set"
-  "inputs" :: "'action signature => 'action set"
-  "outputs" :: "'action signature => 'action set"
-  "internals" :: "'action signature => 'action set"
-  externals :: "'action signature => 'action set"
+definition "outputs" :: "'action signature => 'action set"
+  where asig_outputs_def: "outputs == (fst o snd)"
 
-  is_asig       ::"'action signature => bool"
-  mk_ext_asig   ::"'action signature => 'action signature"
-
-
-defs
+definition "internals" :: "'action signature => 'action set"
+  where asig_internals_def: "internals == (snd o snd)"
 
-asig_inputs_def:    "inputs == fst"
-asig_outputs_def:   "outputs == (fst o snd)"
-asig_internals_def: "internals == (snd o snd)"
+definition "actions" :: "'action signature => 'action set"
+  where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
 
-actions_def:
-   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
-
-externals_def:
-   "externals(asig) == (inputs(asig) Un outputs(asig))"
+definition externals :: "'action signature => 'action set"
+  where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
 
-is_asig_def:
-  "is_asig(triple) ==
-      ((inputs(triple) Int outputs(triple) = {})    &
-       (outputs(triple) Int internals(triple) = {}) &
-       (inputs(triple) Int internals(triple) = {}))"
+definition is_asig :: "'action signature => bool"
+  where "is_asig(triple) ==
+    ((inputs(triple) Int outputs(triple) = {})    &
+     (outputs(triple) Int internals(triple) = {}) &
+     (inputs(triple) Int internals(triple) = {}))"
 
-
-mk_ext_asig_def:
-  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
+definition mk_ext_asig :: "'action signature => 'action signature"
+  where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
 
 
 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/IOA/IOA.thy
--- a/src/HOL/IOA/IOA.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IOA/IOA.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -15,183 +15,148 @@
 type_synonym ('a, 's) transition = "('s * 'a * 's)"
 type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
 
-consts
+(* IO automata *)
+
+definition state_trans :: "['action signature, ('action,'state)transition set] => bool"
+  where "state_trans asig R ==
+     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
+     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+
+definition asig_of :: "('action,'state)ioa => 'action signature"
+  where "asig_of == fst"
 
-  (* IO automata *)
-  state_trans::"['action signature, ('action,'state)transition set] => bool"
-  asig_of    ::"('action,'state)ioa => 'action signature"
-  starts_of  ::"('action,'state)ioa => 'state set"
-  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
-  IOA        ::"('action,'state)ioa => bool"
+definition starts_of :: "('action,'state)ioa => 'state set"
+  where "starts_of == (fst o snd)"
+
+definition trans_of :: "('action,'state)ioa => ('action,'state)transition set"
+  where "trans_of == (snd o snd)"
 
-  (* Executions, schedules, and traces *)
+definition IOA :: "('action,'state)ioa => bool"
+  where "IOA(ioa) == (is_asig(asig_of(ioa)) &
+                (~ starts_of(ioa) = {}) &
+                state_trans (asig_of ioa) (trans_of ioa))"
+
+
+(* Executions, schedules, and traces *)
 
-  is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
-  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
-  executions    :: "('action,'state)ioa => ('action,'state)execution set"
-  mk_trace  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
-  reachable     :: "[('action,'state)ioa, 'state] => bool"
-  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
-  has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
-  traces    :: "('action,'state)ioa => 'action oseq set"
-  NF            :: "'a oseq => 'a oseq"
+(* An execution fragment is modelled with a pair of sequences:
+   the first is the action options, the second the state sequence.
+   Finite executions have None actions from some point on. *)
+definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool"
+  where "is_execution_fragment A ex ==
+     let act = fst(ex); state = snd(ex)
+     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
+              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
+
+definition executions :: "('action,'state)ioa => ('action,'state)execution set"
+  where "executions(ioa) == {e. snd e 0:starts_of(ioa) & is_execution_fragment ioa e}"
 
-  (* Composition of action signatures and automata *)
+
+definition reachable :: "[('action,'state)ioa, 'state] => bool"
+  where "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
+
+definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
+  where "invariant A P == (!s. reachable A s --> P(s))"
+
+
+(* Composition of action signatures and automata *)
+
+consts
   compatible_asigs ::"('a => 'action signature) => bool"
   asig_composition ::"('a => 'action signature) => 'action signature"
   compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
   ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
 
-  (* binary composition of action signatures and automata *)
-  compat_asigs ::"['action signature, 'action signature] => bool"
-  asig_comp    ::"['action signature, 'action signature] => 'action signature"
-  compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
-  par         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
+
+(* binary composition of action signatures and automata *)
 
-  (* Filtering and hiding *)
-  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
+definition compat_asigs ::"['action signature, 'action signature] => bool"
+  where "compat_asigs a1 a2 ==
+   (((outputs(a1) Int outputs(a2)) = {}) &
+    ((internals(a1) Int actions(a2)) = {}) &
+    ((internals(a2) Int actions(a1)) = {}))"
 
-  restrict_asig :: "['a signature, 'a set] => 'a signature"
-  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+definition compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
+  where "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
 
-  (* Notions of correctness *)
-  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
-
-  (* Instantiation of abstract IOA by concrete actions *)
-  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+definition asig_comp :: "['action signature, 'action signature] => 'action signature"
+  where "asig_comp a1 a2 ==
+      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
+        (outputs(a1) Un outputs(a2)),
+        (internals(a1) Un internals(a2))))"
 
-defs
-
-state_trans_def:
-  "state_trans asig R ==
-     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
-     (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+definition par :: "[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
+  where "(ioa1 || ioa2) ==
+     (asig_comp (asig_of ioa1) (asig_of ioa2),
+      {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+      {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+           in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
+              (if a:actions(asig_of(ioa1)) then
+                 (fst(s),a,fst(t)):trans_of(ioa1)
+               else fst(t) = fst(s))
+              &
+              (if a:actions(asig_of(ioa2)) then
+                 (snd(s),a,snd(t)):trans_of(ioa2)
+               else snd(t) = snd(s))})"
 
 
-asig_of_def:   "asig_of == fst"
-starts_of_def: "starts_of == (fst o snd)"
-trans_of_def:  "trans_of == (snd o snd)"
-
-ioa_def:
-  "IOA(ioa) == (is_asig(asig_of(ioa))      &
-                (~ starts_of(ioa) = {})    &
-                state_trans (asig_of ioa) (trans_of ioa))"
-
-
-(* An execution fragment is modelled with a pair of sequences:
- * the first is the action options, the second the state sequence.
- * Finite executions have None actions from some point on.
- *******)
-is_execution_fragment_def:
-  "is_execution_fragment A ex ==
-     let act = fst(ex); state = snd(ex)
-     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
-              (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
-
-
-executions_def:
-  "executions(ioa) == {e. snd e 0:starts_of(ioa) &
-                        is_execution_fragment ioa e}"
-
-
-reachable_def:
-  "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
-
-
-invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
-
+(* Filtering and hiding *)
 
 (* Restrict the trace to those members of the set s *)
-filter_oseq_def:
-  "filter_oseq p s ==
+definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
+  where "filter_oseq p s ==
    (%i. case s(i)
          of None => None
           | Some(x) => if p x then Some x else None)"
 
-
-mk_trace_def:
-  "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
-
+definition mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
+  where "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
 
 (* Does an ioa have an execution with the given trace *)
-has_trace_def:
-  "has_trace ioa b ==
-     (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
+definition has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
+  where "has_trace ioa b == (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
 
-normal_form_def:
-  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
+definition NF :: "'a oseq => 'a oseq"
+  where "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
                     (!j. j ~: range(f) --> nf(j)= None) &
-                    (!i. nf(i)=None --> (nf (Suc i)) = None)   "
+                    (!i. nf(i)=None --> (nf (Suc i)) = None)"
 
 (* All the traces of an ioa *)
-
-  traces_def:
-  "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
-
-(*
-  traces_def:
-  "traces(ioa) == {tr. has_trace ioa tr}"
-*)
-
-compat_asigs_def:
-  "compat_asigs a1 a2 ==
-   (((outputs(a1) Int outputs(a2)) = {}) &
-    ((internals(a1) Int actions(a2)) = {}) &
-    ((internals(a2) Int actions(a1)) = {}))"
-
-
-compat_ioas_def:
-  "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
+definition traces :: "('action,'state)ioa => 'action oseq set"
+  where "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
 
 
-asig_comp_def:
-  "asig_comp a1 a2 ==
-      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
-        (outputs(a1) Un outputs(a2)),
-        (internals(a1) Un internals(a2))))"
-
-
-par_def:
-  "(ioa1 || ioa2) ==
-       (asig_comp (asig_of ioa1) (asig_of ioa2),
-        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
-        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
-             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
-                (if a:actions(asig_of(ioa1)) then
-                   (fst(s),a,fst(t)):trans_of(ioa1)
-                 else fst(t) = fst(s))
-                &
-                (if a:actions(asig_of(ioa2)) then
-                   (snd(s),a,snd(t)):trans_of(ioa2)
-                 else snd(t) = snd(s))})"
-
-
-restrict_asig_def:
-  "restrict_asig asig actns ==
+definition restrict_asig :: "['a signature, 'a set] => 'a signature"
+  where "restrict_asig asig actns ==
     (inputs(asig) Int actns, outputs(asig) Int actns,
      internals(asig) Un (externals(asig) - actns))"
 
-
-restrict_def:
-  "restrict ioa actns ==
+definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+  where "restrict ioa actns ==
     (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
 
 
-ioa_implements_def:
-  "ioa_implements ioa1 ioa2 ==
+
+(* Notions of correctness *)
+
+definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
+  where "ioa_implements ioa1 ioa2 ==
   ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
      (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
       traces(ioa1) <= traces(ioa2))"
 
-rename_def:
-"rename ioa ren ==
-  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
-    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
-    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
-              starts_of(ioa)   ,
-   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
-        in
-        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
+
+(* Instantiation of abstract IOA by concrete actions *)
+
+definition rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+  where "rename ioa ren ==
+    (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
+      {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
+      {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
+                starts_of(ioa)   ,
+     {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
+          in
+          ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
 
 
 declare Let_def [simp]
@@ -206,7 +171,7 @@
 
 lemma trans_in_actions:
   "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
-  apply (unfold ioa_def state_trans_def actions_def is_asig_def)
+  apply (unfold IOA_def state_trans_def actions_def is_asig_def)
   apply (erule conjE)+
   apply (erule allE, erule impE, assumption)
   apply simp
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -26,80 +26,67 @@
 type_synonym 'a item        = "('a, unit) node set"
 type_synonym ('a, 'b) dtree = "('a, 'b) node set"
 
-consts
-  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
-
-  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
-  ndepth    :: "('a, 'b) node => nat"
+definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
+  (*crude "lists" of nats -- needed for the constructions*)
+  where "Push == (%b h. case_nat b h)"
 
-  Atom      :: "('a + nat) => ('a, 'b) dtree"
-  Leaf      :: "'a => ('a, 'b) dtree"
-  Numb      :: "nat => ('a, 'b) dtree"
-  Scons     :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
-  In0       :: "('a, 'b) dtree => ('a, 'b) dtree"
-  In1       :: "('a, 'b) dtree => ('a, 'b) dtree"
-  Lim       :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
-
-  ntrunc    :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
-
-  uprod     :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
-  usum      :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
-
-  Split     :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
-  Case      :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
-
-  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
-                => (('a, 'b) dtree * ('a, 'b) dtree)set"
-  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
-                => (('a, 'b) dtree * ('a, 'b) dtree)set"
+definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
+  where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
 
-defs
+(** operations on S-expressions -- sets of nodes **)
 
-  Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
-
-  (*crude "lists" of nats -- needed for the constructions*)
-  Push_def:   "Push == (%b h. case_nat b h)"
+(*S-expression constructors*)
+definition Atom :: "('a + nat) => ('a, 'b) dtree"
+  where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
+definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
+  where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
 
-  (** operations on S-expressions -- sets of nodes **)
+(*Leaf nodes, with arbitrary or nat labels*)
+definition Leaf :: "'a => ('a, 'b) dtree"
+  where "Leaf == Atom o Inl"
+definition Numb :: "nat => ('a, 'b) dtree"
+  where "Numb == Atom o Inr"
 
-  (*S-expression constructors*)
-  Atom_def:   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
-  Scons_def:  "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
-
-  (*Leaf nodes, with arbitrary or nat labels*)
-  Leaf_def:   "Leaf == Atom o Inl"
-  Numb_def:   "Numb == Atom o Inr"
+(*Injections of the "disjoint sum"*)
+definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
+  where "In0(M) == Scons (Numb 0) M"
+definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
+  where "In1(M) == Scons (Numb 1) M"
 
-  (*Injections of the "disjoint sum"*)
-  In0_def:    "In0(M) == Scons (Numb 0) M"
-  In1_def:    "In1(M) == Scons (Numb 1) M"
+(*Function spaces*)
+definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
+  where "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
 
-  (*Function spaces*)
-  Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
+(*the set of nodes with depth less than k*)
+definition ndepth :: "('a, 'b) node => nat"
+  where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
+definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
+  where "ntrunc k N == {n. n:N & ndepth(n)<k}"
 
-  (*the set of nodes with depth less than k*)
-  ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
-  ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
+(*products and sums for the "universe"*)
+definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
+  where "uprod A B == UN x:A. UN y:B. { Scons x y }"
+definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
+  where "usum A B == In0`A Un In1`B"
 
-  (*products and sums for the "universe"*)
-  uprod_def:  "uprod A B == UN x:A. UN y:B. { Scons x y }"
-  usum_def:   "usum A B == In0`A Un In1`B"
+(*the corresponding eliminators*)
+definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
+  where "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
 
-  (*the corresponding eliminators*)
-  Split_def:  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
-
-  Case_def:   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x))
-                                  | (EX y . M = In1(y) & u = d(y))"
+definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
+  where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))"
 
 
-  (** equality for the "universe" **)
-
-  dprod_def:  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
+(** equality for the "universe" **)
 
-  dsum_def:   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
-                          (UN (y,y'):s. {(In1(y),In1(y'))})"
+definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+      => (('a, 'b) dtree * ('a, 'b) dtree)set"
+  where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
 
+definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+      => (('a, 'b) dtree * ('a, 'b) dtree)set"
+  where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
 
 
 lemma apfst_convE: 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -15,23 +15,26 @@
 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
 
-consts
-  "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
-  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
-  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" 
-(*<*)
+definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+  where "lesub x r y \<longleftrightarrow> r x y"
+
+definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+  where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
+
+definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
+  where "plussub x f y = f x y"
+
 notation (ASCII)
   "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
   "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
   "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
-(*>*)
+
 notation
   "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
   "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
   "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
-(*<*)
+
 (* allow \<sub> instead of \<bsub>..\<esub> *)
-
 abbreviation (input)
   lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
   where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
@@ -43,12 +46,6 @@
 abbreviation (input)
   plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
   where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
-(*>*)
-
-defs
-  lesub_def:   "x \<sqsubseteq>\<^sub>r y \<equiv> r x y"
-  lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y"
-  plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y"
 
 definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where
   "ord r \<equiv> \<lambda>x y. (x,y) \<in> r"
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -82,31 +82,33 @@
 declare Base_not_Xcpt [symmetric, simp]
 declare Ext_not_Xcpt  [symmetric, simp]
 
-consts
-  foo_Base::  java_mb
-  foo_Ext ::  java_mb
-  BaseC   :: "java_mb cdecl"
-  ExtC    :: "java_mb cdecl"
-  test    ::  stmt
-  foo   ::  mname
-  a   ::  loc
-  b       ::  loc
+definition foo_Base :: java_mb
+  where "foo_Base == ([x],[],Skip,LAcc x)"
 
-defs
-  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
-  BaseC_def:"BaseC == (Base, (Object, 
+definition foo_Ext :: java_mb
+  where "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
+               (LAcc x)..vee:=Lit (Intg Numeral1)),
+           Lit Null)"
+
+consts foo ::  mname
+
+definition BaseC :: "java_mb cdecl"
+  where "BaseC == (Base, (Object, 
            [(vee, PrimT Boolean)], 
            [((foo,[Class Base]),Class Base,foo_Base)]))"
-  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
-               (LAcc x)..vee:=Lit (Intg Numeral1)),
-           Lit Null)"
-  ExtC_def: "ExtC  == (Ext,  (Base  , 
+
+definition ExtC :: "java_mb cdecl"
+  where "ExtC  == (Ext,  (Base  ,
            [(vee, PrimT Integer)], 
            [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
-  test_def:"test == Expr(e::=NewC Ext);; 
+definition test ::  stmt
+  where "test == Expr(e::=NewC Ext);;
                     Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
+consts
+  a :: loc
+  b :: loc
 
 abbreviation
   NP  :: xcpt where
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -176,14 +176,18 @@
     by(rule finite_acyclic_wf_converse[OF finite_subcls1])
 qed
 
-consts
-  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
-  field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
-  fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
+definition "method" :: "'c prog \<times> cname => (sig \<rightharpoonup> cname \<times> ty \<times> 'c)"
+  \<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
+  where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
 
-\<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
-defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
-                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
+definition fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list"
+  \<comment> "list of fields of a class, including inherited and hidden ones"
+  where [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
+                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
+
+definition field :: "'c prog \<times> cname => (vname \<rightharpoonup> cname \<times> ty)"
+  where [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
 
 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   method (G,C) = (if C = Object then empty else method (G,D)) ++  
@@ -194,11 +198,6 @@
 apply auto
 done
 
-
-\<comment> "list of fields of a class, including inherited and hidden ones"
-defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
-                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
-
 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
  fields (G,C) = 
   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
@@ -208,9 +207,6 @@
 apply auto
 done
 
-
-defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
-
 lemma field_fields: 
 "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
 apply (unfold field_def)
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -33,24 +33,20 @@
   localT :: "'c env => (vname \<rightharpoonup> ty)"
   where "localT == snd"
 
-consts
-  more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
-                (ty \<times> 'x) \<times> ty list => bool"
-  appl_methds :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
-  max_spec :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
+definition more_spec :: "'c prog \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> bool"
+  where "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
+                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
 
-defs
-  more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
-                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
-  
+definition appl_methds :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
   \<comment> "applicable methods, cf. 15.11.2.1"
-  appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
+  where "appl_methds G C == \<lambda>(mn, pTs).
                      {((Class md,rT),pTs') |md rT mb pTs'.
                       method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
                       list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
 
+definition max_spec :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
   \<comment> "maximally specific methods, cf. 15.11.2.2"
-  max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
+  where "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
                                        (\<forall>m'\<in>appl_methds G C sig.
                                          more_spec G m' m --> m' = m)}"
 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -1273,10 +1273,20 @@
 
 consts inverse :: "'a \<Rightarrow> 'a"
 
-defs (overloaded)
-inverse_bool: "inverse (b::bool) \<equiv> \<not> b"
-inverse_set: "inverse (S::'a set) \<equiv> -S"
-inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
+overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
+begin
+  definition "inverse (b::bool) \<equiv> \<not> b"
+end
+
+overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
+begin
+  definition "inverse (S::'a set) \<equiv> -S"
+end
+
+overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
+begin
+  definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
+end
 
 lemma "inverse b"
 nitpick [expect = genuine]
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -2416,11 +2416,15 @@
 consts
   fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
 
-defs (overloaded)
-  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
-
-defs (overloaded)
-  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
+overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+  definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)"
+end
+
+overloading frsh_star_list \<equiv> "fresh_star :: 'b list \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+  definition fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>set xs. x\<sharp>(c::'a)"
+end
 
 lemmas fresh_star_def = fresh_star_list fresh_star_set
 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/ROOT
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Action.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -9,25 +9,19 @@
 imports Stfun
 begin
 
-
-(** abstract syntax **)
-
-type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
-type_synonym action   = "bool trfun"
+type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a"
+type_synonym action = "bool trfun"
 
 instance prod :: (world, world) world ..
 
-consts
-  (** abstract syntax **)
-  before        :: "'a stfun \<Rightarrow> 'a trfun"
-  after         :: "'a stfun \<Rightarrow> 'a trfun"
-  unch          :: "'a stfun \<Rightarrow> action"
+definition enabled :: "action \<Rightarrow> stpred"
+  where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A"
+
 
-  SqAct         :: "[action, 'a stfun] \<Rightarrow> action"
-  AnAct         :: "[action, 'a stfun] \<Rightarrow> action"
-  enabled       :: "action \<Rightarrow> stpred"
-
-(** concrete syntax **)
+consts
+  before :: "'a stfun \<Rightarrow> 'a trfun"
+  after :: "'a stfun \<Rightarrow> 'a trfun"
+  unch :: "'a stfun \<Rightarrow> action"
 
 syntax
   (* Syntax for writing action expressions in arbitrary contexts *)
@@ -40,8 +34,6 @@
   (*** Priming: same as "after" ***)
   "_prime"      :: "lift \<Rightarrow> lift"                    ("(_`)" [100] 99)
 
-  "_SqAct"      :: "[lift, lift] \<Rightarrow> lift"            ("([_]'_(_))" [0,1000] 99)
-  "_AnAct"      :: "[lift, lift] \<Rightarrow> lift"            ("(<_>'_(_))" [0,1000] 99)
   "_Enabled"    :: "lift \<Rightarrow> lift"                    ("(Enabled _)" [100] 100)
 
 translations
@@ -50,25 +42,30 @@
   "_after"           ==   "CONST after"
   "_prime"           =>   "_after"
   "_unchanged"       ==   "CONST unch"
-  "_SqAct"           ==   "CONST SqAct"
-  "_AnAct"           ==   "CONST AnAct"
   "_Enabled"         ==   "CONST enabled"
-  "w \<Turnstile> [A]_v"       <=   "_SqAct A v w"
-  "w \<Turnstile> <A>_v"       <=   "_AnAct A v w"
   "s \<Turnstile> Enabled A"   <=   "_Enabled A s"
   "w \<Turnstile> unchanged f" <=   "_unchanged f w"
 
 axiomatization where
   unl_before:    "(ACT $v) (s,t) \<equiv> v s" and
   unl_after:     "(ACT v$) (s,t) \<equiv> v t" and
-
   unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
 
-defs
-  square_def:    "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
-  angle_def:     "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
+
+definition SqAct :: "[action, 'a stfun] \<Rightarrow> action"
+  where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)"
+
+definition AnAct :: "[action, 'a stfun] \<Rightarrow> action"
+  where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)"
 
-  enabled_def:   "s \<Turnstile> Enabled A  \<equiv>  \<exists>u. (s,u) \<Turnstile> A"
+syntax
+  "_SqAct" :: "[lift, lift] \<Rightarrow> lift"  ("([_]'_(_))" [0, 1000] 99)
+  "_AnAct" :: "[lift, lift] \<Rightarrow> lift"  ("(<_>'_(_))" [0, 1000] 99)
+translations
+  "_SqAct" == "CONST SqAct"
+  "_AnAct" == "CONST AnAct"
+  "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w"
+  "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w"
 
 
 (* The following assertion specializes "intI" for any world type
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -8,31 +8,35 @@
 imports "../TLA"
 begin
 
-consts
-  (* actions *)
-  BInit     :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
-  Enq       :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
-  Deq       :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
-  Next      :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+(* actions *)
+
+definition BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
+  where "BInit ic q oc == PRED q = #[]"
 
-  (* temporal formulas *)
-  IBuffer   :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
-  Buffer    :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+definition Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "Enq ic q oc == ACT (ic$ \<noteq> $ic)
+                         \<and> (q$ = $q @ [ ic$ ])
+                         \<and> (oc$ = $oc)"
 
-defs
-  BInit_def:   "BInit ic q oc    == PRED q = #[]"
-  Enq_def:     "Enq ic q oc      == ACT (ic$ \<noteq> $ic)
-                                     \<and> (q$ = $q @ [ ic$ ])
-                                     \<and> (oc$ = $oc)"
-  Deq_def:     "Deq ic q oc      == ACT ($q \<noteq> #[])
-                                     \<and> (oc$ = hd< $q >)
-                                     \<and> (q$ = tl< $q >)
-                                     \<and> (ic$ = $ic)"
-  Next_def:    "Next ic q oc     == ACT (Enq ic q oc \<or> Deq ic q oc)"
-  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
-                                      \<and> \<box>[Next ic q oc]_(ic,q,oc)
-                                      \<and> WF(Deq ic q oc)_(ic,q,oc)"
-  Buffer_def:  "Buffer ic oc     == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
+definition Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "Deq ic q oc == ACT ($q \<noteq> #[])
+                         \<and> (oc$ = hd< $q >)
+                         \<and> (q$ = tl< $q >)
+                         \<and> (ic$ = $ic)"
+
+definition Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
+
+
+(* temporal formulas *)
+
+definition IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+  where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
+                                  \<and> \<box>[Next ic q oc]_(ic,q,oc)
+                                  \<and> WF(Deq ic q oc)_(ic,q,oc)"
+
+definition Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+  where "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
 
 
 (* ---------------------------- Data lemmas ---------------------------- *)
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Init.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -16,29 +16,33 @@
 
 type_synonym temporal = "behavior form"
 
-
 consts
-  Initial     :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
   first_world :: "behavior \<Rightarrow> ('w::world)"
   st1         :: "behavior \<Rightarrow> state"
   st2         :: "behavior \<Rightarrow> state"
 
+definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
+  where Init_def: "Initial F sigma = F (first_world sigma)"
+
 syntax
   "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
   "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
-
 translations
   "TEMP F"   => "(F::behavior \<Rightarrow> _)"
   "_Init"    == "CONST Initial"
   "sigma \<Turnstile> Init F"  <= "_Init F sigma"
 
-defs
-  Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
+overloading
+  fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
+  fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
+  fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
+begin
 
-defs (overloaded)
-  fw_temp_def: "first_world == \<lambda>sigma. sigma"
-  fw_stp_def:  "first_world == st1"
-  fw_act_def:  "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
+definition "first_world == \<lambda>sigma. sigma"
+definition "first_world == st1"
+definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
+
+end
 
 lemma const_simps [int_rewrite, simp]:
   "\<turnstile> (Init #True) = #True"
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Intensional.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -17,17 +17,29 @@
 type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a"   (* intention: 'w::world, 'a::type *)
 type_synonym 'w form = "('w, bool) expr"
 
-consts
-  Valid    :: "('w::world) form \<Rightarrow> bool"
-  const    :: "'a \<Rightarrow> ('w::world, 'a) expr"
-  lift     :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
-  lift2    :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
-  lift3    :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
+definition Valid :: "('w::world) form \<Rightarrow> bool"
+  where "Valid A \<equiv> \<forall>w. A w"
+
+definition const :: "'a \<Rightarrow> ('w::world, 'a) expr"
+  where unl_con: "const c w \<equiv> c"
+
+definition lift :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
+  where unl_lift: "lift f x w \<equiv> f (x w)"
+
+definition lift2 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
+  where unl_lift2: "lift2 f x y w \<equiv> f (x w) (y w)"
 
-  (* "Rigid" quantification (logic level) *)
-  RAll     :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"       (binder "Rall " 10)
-  REx      :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"       (binder "Rex " 10)
-  REx1     :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"       (binder "Rex! " 10)
+definition lift3 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
+  where unl_lift3: "lift3 f x y z w \<equiv> f (x w) (y w) (z w)"
+
+(* "Rigid" quantification (logic level) *)
+definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder "Rall " 10)
+  where unl_Rall: "(Rall x. A x) w \<equiv> \<forall>x. A x w"
+definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder "Rex " 10)
+  where unl_Rex: "(Rex x. A x) w \<equiv> \<exists>x. A x w"
+definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"  (binder "Rex! " 10)
+  where unl_Rex1: "(Rex! x. A x) w \<equiv> \<exists>!x. A x w"
+
 
 (** concrete syntax **)
 
@@ -123,8 +135,6 @@
   "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
   "_liftList x"   == "_liftCons x (_const [])"
 
-
-
   "w \<Turnstile> \<not>A"       <= "_liftNot A w"
   "w \<Turnstile> A \<and> B"    <= "_liftAnd A B w"
   "w \<Turnstile> A \<or> B"    <= "_liftOr A B w"
@@ -134,18 +144,6 @@
   "w \<Turnstile> \<exists>x. A"   <= "_REx x A w"
   "w \<Turnstile> \<exists>!x. A"  <= "_REx1 x A w"
 
-defs
-  Valid_def:   "\<turnstile> A    ==  \<forall>w. w \<Turnstile> A"
-
-  unl_con:     "LIFT #c w  ==  c"
-  unl_lift:    "lift f x w == f (x w)"
-  unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
-  unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
-
-  unl_Rall:    "w \<Turnstile> \<forall>x. A x  ==  \<forall>x. (w \<Turnstile> A x)"
-  unl_Rex:     "w \<Turnstile> \<exists>x. A x   ==  \<exists>x. (w \<Turnstile> A x)"
-  unl_Rex1:    "w \<Turnstile> \<exists>!x. A x  ==  \<exists>!x. (w \<Turnstile> A x)"
-
 
 subsection \<open>Lemmas and tactics for "intensional" logics.\<close>
 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -74,10 +74,10 @@
    unanswered call for that process.
 *)
 lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
-  by (auto simp: Return_def MC_action_defs)
+  by (auto simp: AReturn_def MC_action_defs)
 
 lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
-  by (auto simp: Call_def MC_action_defs)
+  by (auto simp: ACall_def MC_action_defs)
 
 
 (* Enabledness of actions *)
@@ -86,7 +86,7 @@
       \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA   
          \<longrightarrow> Enabled (MClkFwd send rcv cst p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
-    @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p)  \<longrightarrow>   
@@ -103,7 +103,7 @@
   apply (tactic \<open>action_simp_tac @{context}
     [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
   apply (tactic \<open>action_simp_tac (@{context} addsimps
-    [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
+    [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}])
     [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -12,122 +12,135 @@
 type_synonym memType = "(Locs \<Rightarrow> Vals) stfun"  (* intention: MemLocs \<Rightarrow> MemVals *)
 type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun"
 
-consts
-  (* state predicates *)
-  MInit      :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
-  PInit      :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
-  (* auxiliary predicates: is there a pending read/write request for
-     some process id and location/value? *)
-  RdRequest  :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
-  WrRequest  :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
+
+(* state predicates *)
+
+definition MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+  where "MInit mm l == PRED mm!l = #InitVal"
+
+definition PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
+  where "PInit rs p == PRED rs!p = #NotAResult"
+
+
+(* auxiliary predicates: is there a pending read/write request for
+   some process id and location/value? *)
+
+definition RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
+  where "RdRequest ch p l == PRED Calling ch p \<and> (arg<ch!p> = #(read l))"
+
+definition WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
+  where "WrRequest ch p l v == PRED Calling ch p \<and> (arg<ch!p> = #(write l v))"
+
+
+(* actions *)
+
+(* a read that doesn't raise BadArg *)
+definition GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "GoodRead mm rs p l == ACT #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
+
+(* a read that raises BadArg *)
+definition BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "BadRead mm rs p l == ACT #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
 
-  (* actions *)
-  GoodRead   :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  BadRead    :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  ReadInner  :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  Read       :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  GoodWrite  :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
-  BadWrite   :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
-  WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
-  Write      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
-  MemReturn  :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  MemFail    :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  RNext      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
-  UNext      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+(* the read action with l visible *)
+definition ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "ReadInner ch mm rs p l == ACT
+    $(RdRequest ch p l)
+    \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
+    \<and> unchanged (rtrner ch ! p)"
+
+(* the read action with l quantified *)
+definition Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
 
-  (* temporal formulas *)
-  RPSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
-  UPSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
-  MSpec      :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
-  IRSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
-  IUSpec     :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+(* similar definitions for the write action *)
+definition GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+  where "GoodWrite mm rs p l v ==
+    ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal
+      \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
 
-  RSpec      :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
-  USpec      :: "memChType \<Rightarrow> temporal"
+definition BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+  where "BadWrite mm rs p l v == ACT
+    \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
+    \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
 
-  (* memory invariant: in the paper, the invariant is hidden in the definition of
-     the predicate S used in the implementation proof, but it is easier to verify
-     at this level. *)
-  MemInv    :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+definition WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+  where "WriteInner ch mm rs p l v == ACT
+    $(WrRequest ch p l v)
+    \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
+    \<and> unchanged (rtrner ch ! p)"
 
-defs
-  MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
-  PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
+definition Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+  where "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
+
 
-  RdRequest_def:     "RdRequest ch p l == PRED
-                         Calling ch p \<and> (arg<ch!p> = #(read l))"
-  WrRequest_def:     "WrRequest ch p l v == PRED
-                         Calling ch p \<and> (arg<ch!p> = #(write l v))"
-  (* a read that doesn't raise BadArg *)
-  GoodRead_def:      "GoodRead mm rs p l == ACT
-                        #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
-  (* a read that raises BadArg *)
-  BadRead_def:       "BadRead mm rs p l == ACT
-                        #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
-  (* the read action with l visible *)
-  ReadInner_def:     "ReadInner ch mm rs p l == ACT
-                         $(RdRequest ch p l)
-                         \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
-                         \<and> unchanged (rtrner ch ! p)"
-  (* the read action with l quantified *)
-  Read_def:          "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
+(* the return action *)
+definition MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "MemReturn ch rs p == ACT
+   (   ($(rs!p) \<noteq> #NotAResult)
+    \<and> ((rs!p)$ = #NotAResult)
+    \<and> Return ch p (rs!p))"
+
+(* the failure action of the unreliable memory *)
+definition MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "MemFail ch rs p == ACT
+    $(Calling ch p)
+    \<and> ((rs!p)$ = #MemFailure)
+    \<and> unchanged (rtrner ch ! p)"
 
-  (* similar definitions for the write action *)
-  GoodWrite_def:     "GoodWrite mm rs p l v == ACT
-                        #l \<in> #MemLoc \<and> #v \<in> #MemVal
-                        \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
-  BadWrite_def:      "BadWrite mm rs p l v == ACT
-                        \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
-                        \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
-  WriteInner_def:    "WriteInner ch mm rs p l v == ACT
-                        $(WrRequest ch p l v)
-                        \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
-                        \<and> unchanged (rtrner ch ! p)"
-  Write_def:         "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
+(* next-state relations for reliable / unreliable memory *)
+definition RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RNext ch mm rs p == ACT
+   (  Read ch mm rs p
+    \<or> (\<exists>l. Write ch mm rs p l)
+    \<or> MemReturn ch rs p)"
+
+definition UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "UNext ch mm rs p == ACT (RNext ch mm rs p \<or> MemFail ch rs p)"
 
-  (* the return action *)
-  MemReturn_def:     "MemReturn ch rs p == ACT
-                       (   ($(rs!p) \<noteq> #NotAResult)
-                        \<and> ((rs!p)$ = #NotAResult)
-                        \<and> Return ch p (rs!p))"
+
+(* temporal formulas *)
+
+definition RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "RPSpec ch mm rs p == TEMP
+    Init(PInit rs p)
+    \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
 
-  (* the failure action of the unreliable memory *)
-  MemFail_def:       "MemFail ch rs p == ACT
-                        $(Calling ch p)
-                        \<and> ((rs!p)$ = #MemFailure)
-                        \<and> unchanged (rtrner ch ! p)"
-  (* next-state relations for reliable / unreliable memory *)
-  RNext_def:         "RNext ch mm rs p == ACT
-                       (  Read ch mm rs p
-                        \<or> (\<exists>l. Write ch mm rs p l)
-                        \<or> MemReturn ch rs p)"
-  UNext_def:         "UNext ch mm rs p == ACT
-                        (RNext ch mm rs p \<or> MemFail ch rs p)"
+definition UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "UPSpec ch mm rs p == TEMP
+    Init(PInit rs p)
+    \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+    \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+    \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+
+definition MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
+  where "MSpec ch mm rs l == TEMP
+    Init(MInit mm l)
+    \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
+
+definition IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+  where "IRSpec ch mm rs == TEMP
+    (\<forall>p. RPSpec ch mm rs p)
+    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
 
-  RPSpec_def:        "RPSpec ch mm rs p == TEMP
-                        Init(PInit rs p)
-                        \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
-                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
-                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
-  UPSpec_def:        "UPSpec ch mm rs p == TEMP
-                        Init(PInit rs p)
-                        \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
-                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
-                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
-  MSpec_def:         "MSpec ch mm rs l == TEMP
-                        Init(MInit mm l)
-                        \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
-  IRSpec_def:        "IRSpec ch mm rs == TEMP
-                        (\<forall>p. RPSpec ch mm rs p)
-                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
-  IUSpec_def:        "IUSpec ch mm rs == TEMP
-                        (\<forall>p. UPSpec ch mm rs p)
-                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+definition IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+  where "IUSpec ch mm rs == TEMP
+    (\<forall>p. UPSpec ch mm rs p)
+    \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+
+definition RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
+  where "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
 
-  RSpec_def:         "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
-  USpec_def:         "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
+definition USpec :: "memChType \<Rightarrow> temporal"
+  where "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
 
-  MemInv_def:        "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
+(* memory invariant: in the paper, the invariant is hidden in the definition of
+   the predicate S used in the implementation proof, but it is easier to verify
+   at this level. *)
+definition MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+  where "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
 
 lemmas RM_action_defs =
   MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
@@ -165,7 +178,7 @@
 *)
 
 lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
-  by (auto simp: Return_def RM_action_defs)
+  by (auto simp: AReturn_def RM_action_defs)
 
 (* Enabledness conditions *)
 
@@ -178,7 +191,7 @@
   apply (tactic
     \<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
   apply (tactic
-    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
+    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
       @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -320,7 +320,7 @@
 (* ==================== Lemmas about the environment ============================== *)
 
 lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
-  by (auto simp: ENext_def Call_def)
+  by (auto simp: ENext_def ACall_def)
 
 (* ==================== Lemmas about the implementation's states ==================== *)
 
@@ -333,7 +333,7 @@
 
 lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
          \<longrightarrow> (S2 rmhist p)$"
-  by (force simp: ENext_def Call_def c_def r_def m_def
+  by (force simp: ENext_def ACall_def c_def r_def m_def
     caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
 
 lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
@@ -352,7 +352,7 @@
          \<longrightarrow> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
     @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
-    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
+    @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
 
 
 (* ------------------------------ State S2 ---------------------------------------- *)
@@ -367,7 +367,7 @@
          \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> (S3 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
-    @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
+    @{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
     @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
@@ -380,7 +380,7 @@
          \<longrightarrow> unchanged (rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
-    MClkReply_def Return_def S_def S2_def)
+    MClkReply_def AReturn_def S_def S2_def)
 
 (* ------------------------------ State S3 ---------------------------------------- *)
 
@@ -405,7 +405,7 @@
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
     @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
-    @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
+    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def},
     @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
     @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -413,7 +413,7 @@
          \<and> unchanged (e p, c p, m p)
          \<longrightarrow> (S6 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
-    @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
+    @{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def},
     @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
     @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -422,7 +422,7 @@
 
 lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
   by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
-    Return_def r_def rtrner_def S_def S3_def Calling_def)
+    AReturn_def r_def rtrner_def S_def S3_def Calling_def)
 
 (* ------------------------------ State S4 ---------------------------------------- *)
 
@@ -441,7 +441,7 @@
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
     @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
-    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
     @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
     @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
@@ -455,7 +455,7 @@
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
     @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
-    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
     @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -471,12 +471,12 @@
 lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
          \<and> HNext rmhist p
          \<longrightarrow> (S5 rmhist p)$"
-  by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
+  by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def
     rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
 
 lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
-    Return_def m_def rtrner_def S_def S4_def Calling_def)
+    AReturn_def m_def rtrner_def S_def S4_def Calling_def)
 
 (* ------------------------------ State S5 ---------------------------------------- *)
 
@@ -493,14 +493,14 @@
 lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
        \<longrightarrow> (S6 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
-    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
+    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
     @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
          \<longrightarrow> (S6 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
-    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
+    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -511,7 +511,7 @@
          \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
-    MClkReply_def Return_def S_def S5_def)
+    MClkReply_def AReturn_def S_def S5_def)
 
 (* ------------------------------ State S6 ---------------------------------------- *)
 
@@ -526,7 +526,7 @@
          \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
-    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
+    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -534,7 +534,7 @@
          \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S1 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
-    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
+    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -545,7 +545,7 @@
   by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
 
 lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
-  by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
+  by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
 
 
 section "Correctness of predicate-action diagram"
@@ -676,7 +676,7 @@
   apply (drule S6_excl [temp_use])
   apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
     apply (force simp: S3_def S_def)
-   apply (auto simp: Return_def)
+   apply (auto simp: AReturn_def)
   done
 
 lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
@@ -724,7 +724,7 @@
     @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
   apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   using [[fast_solver]]
-  apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
+  apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
   done
 
 lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -733,7 +733,7 @@
   apply clarsimp
   apply (drule S5_excl [temp_use] S6_excl [temp_use])+
   apply (auto simp: e_def c_def m_def resbar_def)
-   apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
+   apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
   done
 
 lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -741,7 +741,7 @@
          \<longrightarrow> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])
-  apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
+  apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
    apply (auto simp: S5_def S_def)
   done
 
@@ -752,7 +752,7 @@
   apply (drule S6_excl [temp_use])+
   apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
     @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
-    @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
+    @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
     apply simp_all (* simplify if-then-else *)
     apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
       [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
@@ -909,7 +909,7 @@
 lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
          \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
-    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
+    @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
 
 lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
          \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -1088,7 +1088,7 @@
 lemma MClkReplyS6:
   "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
-    @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
+    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
     @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
 
 lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -16,76 +16,90 @@
   *)
 type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
 
+
+(* data-level functions *)
+
 consts
-  (* data-level functions *)
   cbit          :: "('a,'r) chan \<Rightarrow> bit"
   rbit          :: "('a,'r) chan \<Rightarrow> bit"
   arg           :: "('a,'r) chan \<Rightarrow> 'a"
   res           :: "('a,'r) chan \<Rightarrow> 'r"
 
-  (* state functions *)
-  caller        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
-  rtrner        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
+
+(* state functions *)
 
-  (* state predicates *)
-  Calling   :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+definition caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
+  where "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
 
-  (* actions *)
-  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
-  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+definition rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
+  where "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
+
 
-  (* temporal formulas *)
-  PLegalCaller      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
-  LegalCaller       :: "('a,'r) channel \<Rightarrow> temporal"
-  PLegalReturner    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
-  LegalReturner     :: "('a,'r) channel \<Rightarrow> temporal"
+(* slice through array-valued state function *)
 
-  (* slice through array-valued state function *)
-  slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+definition slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+  where "slice x i s \<equiv> x s i"
 
 syntax
-  "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
-
-  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
-  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
-
+  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  ("(_!_)" [70,70] 70)
 translations
-  "_slice"  ==  "CONST slice"
+  "_slice" \<rightleftharpoons> "CONST slice"
+
+
+(* state predicates *)
+
+definition Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+  where "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
 
-  "_Call"   ==  "CONST ACall"
-  "_Return" ==  "CONST AReturn"
+
+(* actions *)
 
-defs
-  slice_def:     "(PRED (x!i)) s == x s i"
+definition ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "ACall ch p v \<equiv> ACT
+      \<not> $Calling ch p
+    \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
+    \<and> (arg<ch!p>$ = $v)"
 
-  caller_def:    "caller ch   == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
-  rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
+definition AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+  where "AReturn ch p v == ACT
+      $Calling ch p
+    \<and> (rbit<ch!p>$ = $cbit<ch!p>)
+    \<and> (res<ch!p>$ = $v)"
+
+syntax
+  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Call _ _ _)" [90,90,90] 90)
+  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Return _ _ _)" [90,90,90] 90)
+translations
+  "_Call" \<rightleftharpoons> "CONST ACall"
+  "_Return" \<rightleftharpoons> "CONST AReturn"
+
 
-  Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
-  Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
-                                     \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
-                                     \<and> (arg<ch!p>$ = $v)"
-  Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
-                                     \<and> (rbit<ch!p>$ = $cbit<ch!p>)
-                                     \<and> (res<ch!p>$ = $v)"
-  PLegalCaller_def:      "PLegalCaller ch p == TEMP
-                             Init(\<not> Calling ch p)
-                             \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
-  LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
-  PLegalReturner_def:    "PLegalReturner ch p == TEMP
-                                \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
-  LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
+(* temporal formulas *)
+
+definition PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "PLegalCaller ch p == TEMP
+     Init(\<not> Calling ch p)
+     \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+
+definition LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
+  where "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
+
+definition PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "PLegalReturner ch p == TEMP \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
+
+definition LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
+  where "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
 
 declare slice_def [simp]
 
-lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
+lemmas Procedure_defs = caller_def rtrner_def Calling_def ACall_def AReturn_def
   PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
 
 (* Calls and returns change their subchannel *)
 lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
-  by (auto simp: angle_def Call_def caller_def Calling_def)
+  by (auto simp: angle_def ACall_def caller_def Calling_def)
 
 lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
-  by (auto simp: angle_def Return_def rtrner_def Calling_def)
+  by (auto simp: angle_def AReturn_def rtrner_def Calling_def)
 
 end
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -12,63 +12,64 @@
 type_synonym rpcRcvChType = "memChType"
 type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
 
-consts
-  (* state predicates *)
-  RPCInit      :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
+
+(* state predicates *)
 
-  (* actions *)
-  RPCFwd     :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCReject  :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCFail    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCReply   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
-  RPCNext    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
+  where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
+
+
+(* actions *)
 
-  (* temporal *)
-  RPCIPSpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
-  RPCISpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
-
-defs
-  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
+definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCFwd send rcv rst p == ACT
+      $(Calling send p)
+    \<and> $(rst!p) = # rpcA
+    \<and> IsLegalRcvArg<arg<$(send!p)>>
+    \<and> Call rcv p RPCRelayArg<arg<send!p>>
+    \<and> (rst!p)$ = # rpcB
+    \<and> unchanged (rtrner send!p)"
 
-  RPCFwd_def:        "RPCFwd send rcv rst p == ACT
-                         $(Calling send p)
-                         \<and> $(rst!p) = # rpcA
-                         \<and> IsLegalRcvArg<arg<$(send!p)>>
-                         \<and> Call rcv p RPCRelayArg<arg<send!p>>
-                         \<and> (rst!p)$ = # rpcB
-                         \<and> unchanged (rtrner send!p)"
+definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCReject send rcv rst p == ACT
+      $(rst!p) = # rpcA
+    \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
+    \<and> Return send p #BadCall
+    \<and> unchanged ((rst!p), (caller rcv!p))"
 
-  RPCReject_def:     "RPCReject send rcv rst p == ACT
-                           $(rst!p) = # rpcA
-                         \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
-                         \<and> Return send p #BadCall
-                         \<and> unchanged ((rst!p), (caller rcv!p))"
+definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCFail send rcv rst p == ACT
+      \<not>$(Calling rcv p)
+    \<and> Return send p #RPCFailure
+    \<and> (rst!p)$ = #rpcA
+    \<and> unchanged (caller rcv!p)"
 
-  RPCFail_def:       "RPCFail send rcv rst p == ACT
-                           \<not>$(Calling rcv p)
-                         \<and> Return send p #RPCFailure
-                         \<and> (rst!p)$ = #rpcA
-                         \<and> unchanged (caller rcv!p)"
+definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCReply send rcv rst p == ACT
+      \<not>$(Calling rcv p)
+    \<and> $(rst!p) = #rpcB
+    \<and> Return send p res<rcv!p>
+    \<and> (rst!p)$ = #rpcA
+    \<and> unchanged (caller rcv!p)"
 
-  RPCReply_def:      "RPCReply send rcv rst p == ACT
-                           \<not>$(Calling rcv p)
-                         \<and> $(rst!p) = #rpcB
-                         \<and> Return send p res<rcv!p>
-                         \<and> (rst!p)$ = #rpcA
-                         \<and> unchanged (caller rcv!p)"
+definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  where "RPCNext send rcv rst p == ACT
+    (  RPCFwd send rcv rst p
+     \<or> RPCReject send rcv rst p
+     \<or> RPCFail send rcv rst p
+     \<or> RPCReply send rcv rst p)"
+
 
-  RPCNext_def:       "RPCNext send rcv rst p == ACT
-                        (  RPCFwd send rcv rst p
-                         \<or> RPCReject send rcv rst p
-                         \<or> RPCFail send rcv rst p
-                         \<or> RPCReply send rcv rst p)"
+(* temporal *)
 
-  RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
-                           Init RPCInit rcv rst p
-                         \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
-                         \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
+definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  where "RPCIPSpec send rcv rst p == TEMP
+     Init RPCInit rcv rst p
+   \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+   \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
 
-  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
+definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
+  where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
 
 
 lemmas RPC_action_defs =
@@ -82,7 +83,7 @@
 *)
 
 lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
-  by (auto simp: Return_def RPC_action_defs)
+  by (auto simp: AReturn_def RPC_action_defs)
 
 lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
   by (auto simp: RPC_action_defs)
@@ -100,14 +101,14 @@
 lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
     \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
-    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
       \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB  
          \<longrightarrow> Enabled (RPCReply send rcv rst p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
-    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 end
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Memory/RPCParameters.thy
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -16,32 +16,28 @@
 datatype rpcOp = memcall memOp | othercall Vals
 datatype rpcState = rpcA | rpcB
 
-consts
-  (* some particular return values *)
-  RPCFailure     :: Vals
-  BadCall        :: Vals
-  
-  (* Translate an rpc call to a memory call and test if the current argument
-     is legal for the receiver (i.e., the memory). This can now be a little
-     simpler than for the generic RPC component. RelayArg returns an arbitrary
-     memory call for illegal arguments. *)
-  IsLegalRcvArg  :: "rpcOp \<Rightarrow> bool"
-  RPCRelayArg    :: "rpcOp \<Rightarrow> memOp"
-
-axiomatization where
+axiomatization RPCFailure :: Vals and BadCall :: Vals
+where
   (* RPCFailure is different from MemVals and exceptions *)
   RFNoMemVal:        "RPCFailure \<notin> MemVal" and
   NotAResultNotRF:   "NotAResult \<noteq> RPCFailure" and
   OKNotRF:           "OK \<noteq> RPCFailure" and
   BANotRF:           "BadArg \<noteq> RPCFailure"
 
-defs
-  IsLegalRcvArg_def: "IsLegalRcvArg ra ==
-                         case ra of (memcall m) \<Rightarrow> True
-                                  | (othercall v) \<Rightarrow> False"
-  RPCRelayArg_def:   "RPCRelayArg ra ==
-                         case ra of (memcall m) \<Rightarrow> m
-                                  | (othercall v) \<Rightarrow> undefined"
+(* Translate an rpc call to a memory call and test if the current argument
+   is legal for the receiver (i.e., the memory). This can now be a little
+   simpler than for the generic RPC component. RelayArg returns an arbitrary
+   memory call for illegal arguments. *)
+
+definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
+  where "IsLegalRcvArg ra ==
+    case ra of (memcall m) \<Rightarrow> True
+             | (othercall v) \<Rightarrow> False"
+
+definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
+  where "RPCRelayArg ra ==
+    case ra of (memcall m) \<Rightarrow> m
+             | (othercall v) \<Rightarrow> undefined"
 
 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
   NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Stfun.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -40,15 +40,17 @@
   "PRED P"   =>  "(P::state \<Rightarrow> _)"
   "_stvars"  ==  "CONST stvars"
 
-defs
-  (* Base variables may be assigned arbitrary (type-correct) values.
-     Note that vs may be a tuple of variables. The correct identification
-     of base variables is up to the user who must take care not to
-     introduce an inconsistency. For example, "basevars (x,x)" would
-     definitely be inconsistent.
-  *)
-  basevars_def:  "stvars vs == range vs = UNIV"
-
+(* Base variables may be assigned arbitrary (type-correct) values.
+   Note that vs may be a tuple of variables. The correct identification
+   of base variables is up to the user who must take care not to
+   introduce an inconsistency. For example, "basevars (x,x)" would
+   definitely be inconsistent.
+*)
+overloading stvars \<equiv> stvars
+begin
+  definition stvars :: "(state \<Rightarrow> 'a) \<Rightarrow> bool"
+    where basevars_def: "stvars vs == range vs = UNIV"
+end
 
 lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
   apply (unfold basevars_def)
diff -r 18a217591310 -r ec2f0dad8b98 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -894,10 +894,20 @@
 
 consts inverse :: "'a \<Rightarrow> 'a"
 
-defs (overloaded)
-  inverse_bool: "inverse (b::bool)   == ~ b"
-  inverse_set : "inverse (S::'a set) == -S"
-  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
+overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
+begin
+  definition "inverse (b::bool) \<equiv> \<not> b"
+end
+
+overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
+begin
+  definition "inverse (S::'a set) \<equiv> -S"
+end
+
+overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
+begin
+  definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
+end
 
 lemma "inverse b"
 refute [expect = genuine]
diff -r 18a217591310 -r ec2f0dad8b98 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 12 20:05:53 2016 +0100
@@ -7,6 +7,27 @@
 structure Document_Antiquotations: sig end =
 struct
 
+(* Markdown errors *)
+
+local
+
+fun markdown_error binding =
+  Thy_Output.antiquotation binding (Scan.succeed ())
+    (fn {source, ...} => fn _ =>
+      error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
+        Position.here (Position.reset_range (#1 (Token.range_of source)))))
+
+in
+
+val _ =
+  Theory.setup
+   (markdown_error @{binding item} #>
+    markdown_error @{binding enum} #>
+    markdown_error @{binding descr});
+
+end;
+
+
 (* control spacing *)
 
 val _ =
diff -r 18a217591310 -r ec2f0dad8b98 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Sequents/ILL.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -12,14 +12,12 @@
 
   tens :: "[o, o] \<Rightarrow> o"        (infixr "><" 35)
   limp :: "[o, o] \<Rightarrow> o"        (infixr "-o" 45)
-  liff :: "[o, o] \<Rightarrow> o"        (infixr "o-o" 45)
   FShriek :: "o \<Rightarrow> o"          ("! _" [100] 1000)
   lconj :: "[o, o] \<Rightarrow> o"       (infixr "&&" 35)
   ldisj :: "[o, o] \<Rightarrow> o"       (infixr "++" 35)
   zero :: "o"                  ("0")
   top :: "o"                   ("1")
   eye :: "o"                   ("I")
-  aneg :: "o\<Rightarrow>o"               ("~_")
 
 
   (* context manipulation *)
@@ -47,11 +45,11 @@
    (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
 \<close>
 
-defs
+definition liff :: "[o, o] \<Rightarrow> o"  (infixr "o-o" 45)
+  where "P o-o Q == (P -o Q) >< (Q -o P)"
 
-liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
-
-aneg_def:        "~A == A -o 0"
+definition aneg :: "o\<Rightarrow>o"  ("~_")
+  where "~A == A -o 0"
 
 
 axiomatization where
diff -r 18a217591310 -r ec2f0dad8b98 src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Sequents/Modal0.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -12,8 +12,6 @@
 consts
   box           :: "o\<Rightarrow>o"       ("[]_" [50] 50)
   dia           :: "o\<Rightarrow>o"       ("<>_" [50] 50)
-  strimp        :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)
-  streqv        :: "[o,o]\<Rightarrow>o"   (infixr ">-<" 25)
   Lstar         :: "two_seqi"
   Rstar         :: "two_seqi"
 
@@ -36,9 +34,11 @@
   (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
 \<close>
 
-defs
-  strimp_def:    "P --< Q == [](P \<longrightarrow> Q)"
-  streqv_def:    "P >-< Q == (P --< Q) \<and> (Q --< P)"
+definition strimp :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)
+  where "P --< Q == [](P \<longrightarrow> Q)"
+
+definition streqv :: "[o,o]\<Rightarrow>o"   (infixr ">-<" 25)
+  where "P >-< Q == (P --< Q) \<and> (Q --< P)"
 
 
 lemmas rewrite_rls = strimp_def streqv_def
diff -r 18a217591310 -r ec2f0dad8b98 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Jan 12 16:59:32 2016 +0100
+++ b/src/ZF/ZF.thy	Tue Jan 12 20:05:53 2016 +0100
@@ -3,147 +3,262 @@
     Copyright   1993  University of Cambridge
 *)
 
-section\<open>Zermelo-Fraenkel Set Theory\<close>
+section \<open>Zermelo-Fraenkel Set Theory\<close>
 
 theory ZF
 imports "~~/src/FOL/FOL"
 begin
 
+subsection \<open>Signature\<close>
+
 declare [[eta_contract = false]]
 
 typedecl i
 instance i :: "term" ..
 
-axiomatization
-  zero :: "i"  ("0")   \<comment>\<open>the empty set\<close>  and
-  Pow :: "i => i"  \<comment>\<open>power sets\<close>  and
-  Inf :: "i"  \<comment>\<open>infinite set\<close>
+axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>
+  and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>
+  and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
+  and Inf :: "i"  \<comment> \<open>infinite set\<close>
+  and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)
+  and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
+
+abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>
+  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
+
+
+subsection \<open>Bounded Quantifiers\<close>
+
+definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
+  where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
 
-text \<open>Bounded Quantifiers\<close>
-consts
-  Ball   :: "[i, i => o] => o"
-  Bex   :: "[i, i => o] => o"
+definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
+  where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
 
-text \<open>General Union and Intersection\<close>
-axiomatization Union :: "i => i"  ("\<Union>_" [90] 90)
-consts Inter :: "i => i"  ("\<Inter>_" [90] 90)
+syntax
+  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)
+translations
+  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
+  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
+
+
+subsection \<open>Variations on Replacement\<close>
+
+(* Derived form of replacement, restricting P to its functional part.
+   The resulting set (for functional P) is the same as with
+   PrimReplace, but the rules are simpler. *)
+definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
+  where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
 
-text \<open>Variations on Replacement\<close>
-axiomatization PrimReplace :: "[i, [i, i] => o] => i"
-consts
-  Replace     :: "[i, [i, i] => o] => i"
-  RepFun      :: "[i, i => i] => i"
-  Collect     :: "[i, i => o] => i"
+syntax
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
+translations
+  "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
+
+
+(* Functional form of replacement -- analgous to ML's map functional *)
+
+definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
+
+syntax
+  "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])
+translations
+  "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
+
 
-text\<open>Definite descriptions -- via Replace over the set "1"\<close>
-consts
-  The         :: "(i => o) => i"      (binder "THE " 10)
-  If          :: "[o, i, i] => i"     ("(if (_)/ then (_)/ else (_))" [10] 10)
+(* Separation and Pairing can be derived from the Replacement
+   and Powerset Axioms using the following definitions. *)
+definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
+  where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
+
+syntax
+  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")
+translations
+  "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
+
 
-abbreviation (input)
-  old_if      :: "[o, i, i] => i"   ("if '(_,_,_')") where
-  "if(P,a,b) == If(P,a,b)"
+subsection \<open>General union and intersection\<close>
+
+definition Inter :: "i => i"  ("\<Inter>_" [90] 90)
+  where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
+
+syntax
+  "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)
+translations
+  "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
+  "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
 
 
-text \<open>Finite Sets\<close>
-consts
-  Upair :: "[i, i] => i"
-  cons  :: "[i, i] => i"
-  succ  :: "i => i"
+subsection \<open>Finite sets and binary operations\<close>
+
+(*Unordered pairs (Upair) express binary union/intersection and cons;
+  set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
+
+definition Upair :: "[i, i] => i"
+  where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
 
-text \<open>Ordered Pairing\<close>
-consts
-  Pair  :: "[i, i] => i"
-  fst   :: "i => i"
-  snd   :: "i => i"
-  split :: "[[i, i] => 'a, i] => 'a::{}"  \<comment>\<open>for pattern-matching\<close>
+definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>
+  where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
+
+definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>
+  where "A - B == { x\<in>A . ~(x\<in>B) }"
 
-text \<open>Sigma and Pi Operators\<close>
-consts
-  Sigma :: "[i, i => i] => i"
-  Pi    :: "[i, i => i] => i"
+definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>
+  where "A \<union> B == \<Union>(Upair(A,B))"
+
+definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>
+  where "A \<inter> B == \<Inter>(Upair(A,B))"
 
-text \<open>Relations and Functions\<close>
-consts
-  "domain"    :: "i => i"
-  range       :: "i => i"
-  field       :: "i => i"
-  converse    :: "i => i"
-  relation    :: "i => o"        \<comment>\<open>recognizes sets of pairs\<close>
-  "function"  :: "i => o"        \<comment>\<open>recognizes functions; can have non-pairs\<close>
-  Lambda      :: "[i, i => i] => i"
-  restrict    :: "[i, i] => i"
+definition cons :: "[i, i] => i"
+  where "cons(a,A) == Upair(a,a) \<union> A"
+
+definition succ :: "i => i"
+  where "succ(i) == cons(i, i)"
 
-text \<open>Infixes in order of decreasing precedence\<close>
-consts
-  Image       :: "[i, i] => i"    (infixl "``" 90) \<comment>\<open>image\<close>
-  vimage      :: "[i, i] => i"    (infixl "-``" 90) \<comment>\<open>inverse image\<close>
-  "apply"     :: "[i, i] => i"    (infixl "`" 90) \<comment>\<open>function application\<close>
-  "Int"       :: "[i, i] => i"    (infixl "\<inter>" 70) \<comment>\<open>binary intersection\<close>
-  "Un"        :: "[i, i] => i"    (infixl "\<union>" 65) \<comment>\<open>binary union\<close>
-  Diff        :: "[i, i] => i"    (infixl "-" 65) \<comment>\<open>set difference\<close>
-  Subset      :: "[i, i] => o"    (infixl "\<subseteq>" 50) \<comment>\<open>subset relation\<close>
+nonterminal "is"
+syntax
+  "" :: "i \<Rightarrow> is"  ("_")
+  "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")
+  "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")
+translations
+  "{x, xs}" == "CONST cons(x, {xs})"
+  "{x}" == "CONST cons(x, 0)"
+
+
+subsection \<open>Axioms\<close>
+
+(* ZF axioms -- see Suppes p.238
+   Axioms for Union, Pow and Replace state existence only,
+   uniqueness is derivable using extensionality. *)
 
 axiomatization
-  mem         :: "[i, i] => o"    (infixl "\<in>" 50) \<comment>\<open>membership relation\<close>
-
-abbreviation
-  not_mem :: "[i, i] => o"  (infixl "\<notin>" 50)  \<comment>\<open>negated membership relation\<close>
-  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
+where
+  extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
+  Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
+  Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
 
-abbreviation
-  cart_prod :: "[i, i] => i"    (infixr "\<times>" 80) \<comment>\<open>Cartesian product\<close>
-  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
+  (*We may name this set, though it is not uniquely defined.*)
+  infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
 
-abbreviation
-  function_space :: "[i, i] => i"  (infixr "->" 60) \<comment>\<open>function space\<close>
-  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
+  (*This formulation facilitates case analysis on A.*)
+  foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
+
+  (*Schema axiom since predicate P is a higher-order variable*)
+  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
+                         b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
 
 
-nonterminal "is" and patterns
+subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
+
+definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)
+  where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
 
-syntax
-  ""          :: "i => is"                   ("_")
-  "_Enum"     :: "[i, is] => is"             ("_,/ _")
+definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)
+  where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
+
+abbreviation (input)
+  old_if :: "[o, i, i] => i"  ("if '(_,_,_')")
+  where "if(P,a,b) == If(P,a,b)"
+
+
+subsection \<open>Ordered Pairing\<close>
 
-  "_Finset"   :: "is => i"                   ("{(_)}")
-  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
-  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
-  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
-  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
-  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
+(* this "symmetric" definition works better than {{a}, {a,b}} *)
+definition Pair :: "[i, i] => i"
+  where "Pair(a,b) == {{a,a}, {a,b}}"
+
+definition fst :: "i \<Rightarrow> i"
+  where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
 
-  (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
+definition snd :: "i \<Rightarrow> i"
+  where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
 
+definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
+  where "split(c) == \<lambda>p. c(fst(p), snd(p))"
+
+(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
+nonterminal patterns
+syntax
   "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
   ""          :: "pttrn => patterns"         ("_")
   "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
-
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
 translations
-  "{x, xs}"     == "CONST cons(x, {xs})"
-  "{x}"         == "CONST cons(x, 0)"
-  "{x\<in>A. P}"    == "CONST Collect(A, \<lambda>x. P)"
-  "{y. x\<in>A, Q}" == "CONST Replace(A, \<lambda>x y. Q)"
-  "{b. x\<in>A}"    == "CONST RepFun(A, \<lambda>x. b)"
-  "\<Inter>x\<in>A. B"    == "CONST Inter({B. x\<in>A})"
-  "\<Union>x\<in>A. B"    == "CONST Union({B. x\<in>A})"
-  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
-  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
-  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
-  "\<forall>x\<in>A. P"    == "CONST Ball(A, \<lambda>x. P)"
-  "\<exists>x\<in>A. P"    == "CONST Bex(A, \<lambda>x. P)"
-
   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
   "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
   "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
 
+definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
+
+abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>
+  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
+
+
+subsection \<open>Relations and Functions\<close>
+
+(*converse of relation r, inverse of function*)
+definition converse :: "i \<Rightarrow> i"
+  where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
+
+definition domain :: "i \<Rightarrow> i"
+  where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
+
+definition range :: "i \<Rightarrow> i"
+  where "range(r) == domain(converse(r))"
+
+definition field :: "i \<Rightarrow> i"
+  where "field(r) == domain(r) \<union> range(r)"
+
+definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
+  where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
+
+definition function :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
+  where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
+
+definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>
+  where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
+
+definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>
+  where vimage_def: "r -`` A == converse(r)``A"
+
+(* Restrict the relation r to the domain A *)
+definition restrict :: "[i, i] \<Rightarrow> i"
+  where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
+
+
+(* Abstraction, application and Cartesian product of a family of sets *)
+
+definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
+
+definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>
+  where "f`a == \<Union>(f``{a})"
+
+definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
+
+abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>
+  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
+
+
+(* binder syntax *)
+
+syntax
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+translations
+  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
+  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
+  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
+
+
+subsection \<open>ASCII syntax\<close>
 
 notation (ASCII)
   cart_prod       (infixr "*" 80) and
@@ -155,6 +270,8 @@
   not_mem         (infixl "~:" 50)
 
 syntax (ASCII)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
   "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
   "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
   "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
@@ -163,104 +280,9 @@
   "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
   "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
   "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
   "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
   "_pattern"  :: "patterns => pttrn"         ("<_>")
 
-defs  (* Bounded Quantifiers *)
-  Ball_def:      "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
-  Bex_def:       "Bex(A, P) == \<exists>x. x\<in>A & P(x)"
-
-  subset_def:    "A \<subseteq> B == \<forall>x\<in>A. x\<in>B"
-
-
-axiomatization where
-
-  (* ZF axioms -- see Suppes p.238
-     Axioms for Union, Pow and Replace state existence only,
-     uniqueness is derivable using extensionality. *)
-
-  extension:     "A = B <-> A \<subseteq> B & B \<subseteq> A" and
-  Union_iff:     "A \<in> \<Union>(C) <-> (\<exists>B\<in>C. A\<in>B)" and
-  Pow_iff:       "A \<in> Pow(B) <-> A \<subseteq> B" and
-
-  (*We may name this set, though it is not uniquely defined.*)
-  infinity:      "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
-
-  (*This formulation facilitates case analysis on A.*)
-  foundation:    "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
-
-  (*Schema axiom since predicate P is a higher-order variable*)
-  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) \<longrightarrow> y=z) ==>
-                         b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))"
-
-
-defs
-
-  (* Derived form of replacement, restricting P to its functional part.
-     The resulting set (for functional P) is the same as with
-     PrimReplace, but the rules are simpler. *)
-
-  Replace_def:  "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
-
-  (* Functional form of replacement -- analgous to ML's map functional *)
-
-  RepFun_def:   "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
-
-  (* Separation and Pairing can be derived from the Replacement
-     and Powerset Axioms using the following definitions. *)
-
-  Collect_def:  "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
-
-  (*Unordered pairs (Upair) express binary union/intersection and cons;
-    set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
-
-  Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
-  cons_def:  "cons(a,A) == Upair(a,a) \<union> A"
-  succ_def:  "succ(i) == cons(i, i)"
-
-  (* Difference, general intersection, binary union and small intersection *)
-
-  Diff_def:      "A - B    == { x\<in>A . ~(x\<in>B) }"
-  Inter_def:     "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
-  Un_def:        "A \<union>  B  == \<Union>(Upair(A,B))"
-  Int_def:      "A \<inter> B  == \<Inter>(Upair(A,B))"
-
-  (* definite descriptions *)
-  the_def:      "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
-  if_def:       "if(P,a,b) == THE z. P & z=a | ~P & z=b"
-
-  (* this "symmetric" definition works better than {{a}, {a,b}} *)
-  Pair_def:     "<a,b>  == {{a,a}, {a,b}}"
-  fst_def:      "fst(p) == THE a. \<exists>b. p=<a,b>"
-  snd_def:      "snd(p) == THE b. \<exists>a. p=<a,b>"
-  split_def:    "split(c) == %p. c(fst(p), snd(p))"
-  Sigma_def:    "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x,y>}"
-
-  (* Operations on relations *)
-
-  (*converse of relation r, inverse of function*)
-  converse_def: "converse(r) == {z. w\<in>r, \<exists>x y. w=<x,y> & z=<y,x>}"
-
-  domain_def:   "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}"
-  range_def:    "range(r) == domain(converse(r))"
-  field_def:    "field(r) == domain(r) \<union> range(r)"
-  relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>"
-  function_def: "function(r) ==
-                    \<forall>x y. <x,y>:r \<longrightarrow> (\<forall>y'. <x,y'>:r \<longrightarrow> y=y')"
-  image_def:    "r `` A  == {y \<in> range(r) . \<exists>x\<in>A. <x,y> \<in> r}"
-  vimage_def:   "r -`` A == converse(r)``A"
-
-  (* Abstraction, application and Cartesian product of a family of sets *)
-
-  lam_def:      "Lambda(A,b) == {<x,b(x)> . x\<in>A}"
-  apply_def:    "f`a == \<Union>(f``{a})"
-  Pi_def:       "Pi(A,B)  == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
-
-  (* Restrict the relation r to the domain A *)
-  restrict_def: "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
-
 
 subsection \<open>Substitution\<close>