# HG changeset patch
# User wenzelm
# Date 1298045119 -3600
# Node ID 7eb9eac392b698d0de3064b8d05f489da87d3d00
# Parent  22d23da89aa518a90e202f55d559dc3af3b62c14# Parent  a68f503805ed9a97598c602e4e4b4ce8753d4df1
merged

diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/FOL.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -18,7 +18,7 @@
 
 subsection {* The classical axiom *}
 
-axioms
+axiomatization where
   classical: "(~P ==> P) ==> P"
 
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/IFOL.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -88,42 +88,39 @@
 finalconsts
   False All Ex eq conj disj imp
 
-axioms
-
+axiomatization where
   (* Equality *)
-
-  refl:         "a=a"
+  refl:         "a=a" and
   subst:        "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
 
+
+axiomatization where
   (* Propositional logic *)
-
-  conjI:        "[| P;  Q |] ==> P&Q"
-  conjunct1:    "P&Q ==> P"
-  conjunct2:    "P&Q ==> Q"
+  conjI:        "[| P;  Q |] ==> P&Q" and
+  conjunct1:    "P&Q ==> P" and
+  conjunct2:    "P&Q ==> Q" and
 
-  disjI1:       "P ==> P|Q"
-  disjI2:       "Q ==> P|Q"
-  disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
+  disjI1:       "P ==> P|Q" and
+  disjI2:       "Q ==> P|Q" and
+  disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R" and
 
-  impI:         "(P ==> Q) ==> P-->Q"
-  mp:           "[| P-->Q;  P |] ==> Q"
+  impI:         "(P ==> Q) ==> P-->Q" and
+  mp:           "[| P-->Q;  P |] ==> Q" and
 
   FalseE:       "False ==> P"
 
+axiomatization where
   (* Quantifiers *)
+  allI:         "(!!x. P(x)) ==> (ALL x. P(x))" and
+  spec:         "(ALL x. P(x)) ==> P(x)" and
 
-  allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
-  spec:         "(ALL x. P(x)) ==> P(x)"
-
-  exI:          "P(x) ==> (EX x. P(x))"
+  exI:          "P(x) ==> (EX x. P(x))" and
   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
 
 
-axioms
-
+axiomatization where
   (* Reflection, admissible *)
-
-  eq_reflection:  "(x=y)   ==> (x==y)"
+  eq_reflection:  "(x=y)   ==> (x==y)" and
   iff_reflection: "(P<->Q) ==> (P==Q)"
 
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/If.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOL/ex/If.ML
+(*  Title:      FOL/ex/If.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -13,10 +13,10 @@
   zero :: int ("0")
   minus :: "int => int" ("- _")
 
-axioms
-  int_assoc: "(x + y::int) + z = x + (y + z)"
-  int_zero: "0 + x = x"
-  int_minus: "(-x) + x = 0"
+axiomatization where
+  int_assoc: "(x + y::int) + z = x + (y + z)" and
+  int_zero: "0 + x = x" and
+  int_minus: "(-x) + x = 0" and
   int_minus2: "-(-x) = x"
 
 section {* Inference of parameter types *}
@@ -527,13 +527,12 @@
 
 end
 
-consts
-  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
-  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
-
-axioms
-  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
-  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
+axiomatization
+  gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
+  gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
+where
+  grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
+  grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
 
 text {* Setup *}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Nat.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -12,21 +12,19 @@
 typedecl nat
 arities nat :: "term"
 
-consts
-  Zero :: nat    ("0")
-  Suc :: "nat => nat"
+axiomatization
+  Zero :: nat  ("0") and
+  Suc :: "nat => nat" and
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
-  add :: "[nat, nat] => nat"    (infixl "+" 60)
+where
+  induct: "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)" and
+  Suc_inject: "Suc(m)=Suc(n) ==> m=n" and
+  Suc_neq_0: "Suc(m)=0 ==> R" and
+  rec_0: "rec(0,a,f) = a" and
+  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
 
-axioms
-  induct:      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
-  Suc_inject:  "Suc(m)=Suc(n) ==> m=n"
-  Suc_neq_0:   "Suc(m)=0      ==> R"
-  rec_0:       "rec(0,a,f) = a"
-  rec_Suc:     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-
-defs
-  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
+definition add :: "[nat, nat] => nat"  (infixl "+" 60)
+  where "m + n == rec(m, n, %x y. Suc(y))"
 
 
 subsection {* Proofs about the natural numbers *}
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Prolog.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -11,15 +11,16 @@
 
 typedecl 'a list
 arities list :: ("term") "term"
-consts
-  Nil     :: "'a list"
-  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60)
-  app     :: "['a list, 'a list, 'a list] => o"
+
+axiomatization
+  Nil     :: "'a list" and
+  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60) and
+  app     :: "['a list, 'a list, 'a list] => o" and
   rev     :: "['a list, 'a list] => o"
-axioms
-  appNil:  "app(Nil,ys,ys)"
-  appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
-  revNil:  "rev(Nil,Nil)"
+where
+  appNil:  "app(Nil,ys,ys)" and
+  appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and
+  revNil:  "rev(Nil,Nil)" and
   revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
 
 schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOL/ex/Quantifiers_Cla.thy
--- a/src/FOL/ex/Quantifiers_Cla.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOL/ex/Quantifiers_Cla.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOL/ex/Quantifiers_Int.thy
+(*  Title:      FOL/ex/Quantifiers_Cla.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOLP/FOLP.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -11,10 +11,8 @@
   ("classical.ML") ("simp.ML") ("simpdata.ML")
 begin
 
-consts
-  cla :: "[p=>p]=>p"
-axioms
-  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+axiomatization cla :: "[p=>p]=>p"
+  where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
 
 
 (*** Classical introduction rules for | and EX ***)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOLP/ex/Foundation.thy
--- a/src/FOLP/ex/Foundation.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOLP/ex/Foundation.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ex/Foundation.ML
+(*  Title:      FOLP/ex/Foundation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/FOLP/ex/Nat.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ex/nat.thy
+(*  Title:      FOLP/ex/Nat.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Analz.thy
--- a/src/HOL/Auth/Guard/Analz.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: december 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Analz.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2001  University of Cambridge
+*)
 
 header{*Decomposition of Analz into two parts*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Extensions.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2001  University of Cambridge
+*)
 
 header {*Extensions to Standard Theories*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: january 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Guard.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
 
 header{*Protocol-Independent Confidentiality Theorem on Nonces*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,18 +1,12 @@
-(******************************************************************************
-very similar to Guard except:
+(*  Title:      HOL/Auth/Guard/GuardK.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Very similar to Guard except:
 - Guard is replaced by GuardK, guard by guardK, Nonce by Key
 - some scripts are slightly modified (+ keyset_in, kparts_parts)
 - the hypothesis Key n ~:G (keyset G) is added
-
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+*)
 
 header{*protocol-independent confidentiality theorem on keys*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Guard_NS_Public.thy
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-incorporating Lowe's fix (inclusion of B's identity in round 2)
+(*  Title:      HOL/Auth/Guard/Guard_NS_Public.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
 
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Incorporating Lowe's fix (inclusion of B's identity in round 2).
+*)
 
 header{*Needham-Schroeder-Lowe Public-Key Protocol*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Guard_OtwayRees.thy
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Guard_OtwayRees.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
 
 header{*Otway-Rees Protocol*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Guard_Public.thy
--- a/src/HOL/Auth/Guard/Guard_Public.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-lemmas on guarded messages for public protocols
+(*  Title:      HOL/Auth/Guard/Guard_Public.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
 
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Lemmas on guarded messages for public protocols.
+*)
 
 theory Guard_Public imports Guard Public Extensions begin
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Guard_Shared.thy
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Guard_Shared.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
 
 header{*lemmas on guarded messages for protocols with symmetric keys*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Guard_Yahalom.thy
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Guard_Yahalom.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
 
 header{*Yahalom Protocol*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/List_Msg.thy
--- a/src/HOL/Auth/Guard/List_Msg.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/List_Msg.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2001  University of Cambridge
+*)
 
 header{*Lists of Messages and Lists of Agents*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/P1.thy
--- a/src/HOL/Auth/Guard/P1.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/P1.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(*  Title:      HOL/Auth/Guard/P1.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
 
-date: february 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
 
 header{*Protocol P1*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/P2.thy
--- a/src/HOL/Auth/Guard/P2.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/P2.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(*  Title:      HOL/Auth/Guard/P2.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
 
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
 
 header{*Protocol P2*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: april 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(*  Title:      HOL/Auth/Guard/Proto.thy
+    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
+    Copyright   2002  University of Cambridge
+*)
 
 header{*Other Protocol-Independent Results*}
 
@@ -15,13 +9,13 @@
 
 subsection{*protocols*}
 
-types rule = "event set * event"
+type_synonym rule = "event set * event"
 
 abbreviation
   msg' :: "rule => msg" where
   "msg' R == msg (snd R)"
 
-types proto = "rule set"
+type_synonym proto = "rule set"
 
 definition wdef :: "proto => bool" where
 "wdef p == ALL R k. R:p --> Number k:parts {msg' R}
@@ -155,9 +149,9 @@
 
 subsection{*types*}
 
-types keyfun = "rule => subs => nat => event list => key set"
+type_synonym keyfun = "rule => subs => nat => event list => key set"
 
-types secfun = "rule => nat => subs => key set => msg"
+type_synonym secfun = "rule => nat => subs => key set => msg"
 
 subsection{*introduction of a fresh guarded nonce*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/KerberosIV.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
   Tgs :: agent where "Tgs == Friend 0"
 
 
-axioms
+axiomatization where
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/KerberosIV_Gets.thy
--- a/src/HOL/Auth/KerberosIV_Gets.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
   Tgs :: agent where "Tgs == Friend 0"
 
 
-axioms
+axiomatization where
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/KerberosV.thy
--- a/src/HOL/Auth/KerberosV.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/KerberosV.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -17,7 +17,7 @@
   "Tgs == Friend 0"
 
 
-axioms
+axiomatization where
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
 by blast
 
-types 
+type_synonym
   key = nat
 
 consts
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Public.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -68,7 +68,7 @@
    done                       
 
 
-axioms
+axiomatization where
   (*No private key equals any public key (essential to ensure that private
     keys are private!) *)
   privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
@@ -141,7 +141,7 @@
    apply (simp add: inj_on_def split: agent.split) 
    done
 
-axioms
+axiomatization where
   sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
 
 text{*Injectiveness: Agents' long-term keys are distinct.*}
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -5,24 +5,19 @@
 
 theory ShoupRubin imports Smartcard begin
 
-consts
-
-    sesK :: "nat*key => key"
-
-axioms
-     
+axiomatization sesK :: "nat*key => key"
+where
    (*sesK is injective on each component*) 
-   inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
-
+   inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
    (*all long-term keys differ from sesK*)
-   shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
-   crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
-   pin_disj_sesK  [iff]: "pin P \<noteq> sesK(m,pk)"
-   pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)"
+   shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+   crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+   pin_disj_sesK  [iff]: "pin P \<noteq> sesK(m,pk)" and
+   pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)" and
 
    (*needed for base case in analz_image_freshK*)
    Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
-                   Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" 
+                   Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
 
   (*this protocol makes the assumption of secure means
     between each agent and his smartcard*)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -11,24 +11,20 @@
 Availability. Only the updated version makes the goals of confidentiality,
 authentication and key distribution available to both peers.*}
 
-consts
-
-    sesK :: "nat*key => key"
-
-axioms
-     
+axiomatization sesK :: "nat*key => key"
+where
    (*sesK is injective on each component*) 
-   inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
+   inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
 
    (*all long-term keys differ from sesK*)
-   shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
-   crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
-   pin_disj_sesK  [iff]: "pin P \<noteq> sesK(m,pk)"
-   pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)"
+   shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+   crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+   pin_disj_sesK  [iff]: "pin P \<noteq> sesK(m,pk)" and
+   pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)" and
 
    (*needed for base case in analz_image_freshK*)
    Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
-                   Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" 
+                   Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
 
   (*this protocol makes the assumption of secure means
     between each agent and his smartcard*)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -16,31 +16,30 @@
 smartcard, which independently may be stolen or cloned.
 *}
 
-consts
-  shrK    :: "agent => key"  (*long-term keys saved in smart cards*)
-  crdK    :: "card  => key"  (*smart cards' symmetric keys*)
-  pin     :: "agent => key"  (*pin to activate the smart cards*)
+axiomatization
+  shrK    :: "agent => key" and  (*long-term keys saved in smart cards*)
+  crdK    :: "card  => key" and  (*smart cards' symmetric keys*)
+  pin     :: "agent => key" and  (*pin to activate the smart cards*)
 
   (*Mostly for Shoup-Rubin*)
-  Pairkey :: "agent * agent => nat"
+  Pairkey :: "agent * agent => nat" and
   pairK   :: "agent * agent => key"
-
-axioms
-  inj_shrK: "inj shrK"  --{*No two smartcards store the same key*}
-  inj_crdK: "inj crdK"  --{*Nor do two cards*}
-  inj_pin : "inj pin"   --{*Nor do two agents have the same pin*}
+where
+  inj_shrK: "inj shrK" and  --{*No two smartcards store the same key*}
+  inj_crdK: "inj crdK" and  --{*Nor do two cards*}
+  inj_pin : "inj pin" and   --{*Nor do two agents have the same pin*}
 
   (*pairK is injective on each component, if we assume encryption to be a PRF
     or at least collision free *)
-  inj_pairK    [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
-  comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
+  inj_pairK    [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')" and
+  comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)" and
 
   (*long-term keys differ from each other*)
-  pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
-  pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
-  pairK_disj_pin [iff]:  "pairK(A,B) \<noteq> pin P"
-  shrK_disj_crdK [iff]:  "shrK P \<noteq> crdK C"
-  shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q"
+  pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C" and
+  pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P" and
+  pairK_disj_pin [iff]:  "pairK(A,B) \<noteq> pin P" and
+  shrK_disj_crdK [iff]:  "shrK P \<noteq> crdK C" and
+  shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q" and
   crdK_disj_pin [iff]:   "crdK C \<noteq> pin P"
 
 definition legalUse :: "card => bool" ("legalUse (_)") where
@@ -78,8 +77,8 @@
 end
 
 text{*Still relying on axioms*}
-axioms
-  Key_supply_ax:  "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
+axiomatization where
+  Key_supply_ax:  "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs" and
 
   (*Needed because of Spy's knowledge of Pairkeys*)
   Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
@@ -129,7 +128,7 @@
 (*Specialized to shared-key model: no @{term invKey}*)
 lemma keysFor_parts_insert:
      "\<lbrakk> K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) \<rbrakk> 
-     \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+     \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
 by (force dest: EventSC.keysFor_parts_insert)  
 
 lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Auth/TLS.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -86,9 +86,9 @@
    apply (simp add: inj_on_def prod_encode_eq split: role.split) 
    done
 
-axioms
+axiomatization where
   --{*sessionK makes symmetric keys*}
-  isSym_sessionK: "sessionK nonces \<in> symKeys"
+  isSym_sessionK: "sessionK nonces \<in> symKeys" and
 
   --{*sessionK never clashes with a long-term symmetric key  
      (they don't exist in TLS anyway)*}
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/AxSem.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -36,7 +36,7 @@
 \end{itemize}
 *}
 
-types  res = vals --{* result entry *}
+type_synonym  res = vals --{* result entry *}
 
 abbreviation (input)
   Val where "Val x == In1 x"
@@ -58,7 +58,7 @@
   "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
 
   --{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
 translations
   (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
 
@@ -381,7 +381,7 @@
 datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
 something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
                                         ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
-types    'a triples = "'a triple set"
+type_synonym 'a triples = "'a triple set"
 
 abbreviation
   var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Conform.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -16,7 +16,7 @@
 \end{itemize}
 *}
 
-types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
 
 
 section "extension of global store"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Decl.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -136,7 +136,7 @@
 
 
 subsubsection {* Static Modifier *}
-types stat_modi = bool (* modifier: static *)
+type_synonym stat_modi = bool (* modifier: static *)
 
 subsection {* Declaration (base "class" for member,interface and class
  declarations *}
@@ -164,8 +164,7 @@
   (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
   (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
 
-types     
-        fdecl           (* field declaration, cf. 8.3 *)
+type_synonym fdecl          (* field declaration, cf. 8.3 *)
         = "vname \<times> field"
 
 
@@ -185,7 +184,7 @@
 record methd = mhead + (* method in a class *)
         mbody::mbody
 
-types mdecl = "sig \<times> methd"  (* method declaration in a class *)
+type_synonym mdecl = "sig \<times> methd"  (* method declaration in a class *)
 
 
 translations
@@ -300,7 +299,7 @@
 
 record  iface = ibody + --{* interface *}
          isuperIfs:: "qtname list" --{* superinterface list *}
-types
+type_synonym
         idecl           --{* interface declaration, cf. 9.1 *}
         = "qtname \<times> iface"
 
@@ -332,7 +331,7 @@
 record "class" = cbody +           --{* class *}
         super   :: "qtname"      --{* superclass *}
         superIfs:: "qtname list" --{* implemented interfaces *}
-types
+type_synonym
         cdecl           --{* class declaration, cf. 8.1 *}
         = "qtname \<times> class"
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1401,7 +1401,7 @@
 section "fields and methods"
 
 
-types
+type_synonym
   fspec = "vname \<times> qtname"
 
 translations 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -498,7 +498,7 @@
 section "The rules of definite assignment"
 
  
-types breakass = "(label, lname) tables" 
+type_synonym breakass = "(label, lname) tables" 
 --{* Mapping from a break label, to the set of variables that will be assigned 
      if the evaluation terminates with this break *}
     
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Eval.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -96,8 +96,8 @@
 *}
 
 
-types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
-      vals  =        "(val, vvar, val list) sum3"
+type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+type_synonym vals = "(val, vvar, val list) sum3"
 translations
   (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   (type) "vals" <= (type) "(val, vvar, val list) sum3" 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/State.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -27,7 +27,7 @@
                            since its type is given already by the reference to 
                            it (see below) *}
 
-types   vn   = "fspec + int"                    --{* variable name      *}
+type_synonym vn = "fspec + int"                 --{* variable name      *}
 record  obj  = 
           tag :: "obj_tag"                      --{* generalized object *}
           "values" :: "(vn, val) table"      
@@ -130,7 +130,7 @@
 
 section "object references"
 
-types oref = "loc + qtname"         --{* generalized object reference *}
+type_synonym oref = "loc + qtname"         --{* generalized object reference *}
 syntax
   Heap  :: "loc   \<Rightarrow> oref"
   Stat  :: "qtname \<Rightarrow> oref"
@@ -213,11 +213,11 @@
 
 section "stores"
 
-types   globs               --{* global variables: heap and static variables *}
+type_synonym globs               --{* global variables: heap and static variables *}
         = "(oref , obj) table"
-        heap
+type_synonym heap
         = "(loc  , obj) table"
-(*      locals                   
+(* type_synonym locals                   
         = "(lname, val) table" *) (* defined in Value.thy local variables *)
 
 translations
@@ -579,7 +579,7 @@
 
 section "full program state"
 
-types
+type_synonym
   state = "abopt \<times> st"          --{* state including abruption information *}
 
 translations
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Table.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -29,9 +29,9 @@
 \end{itemize}
 *}
 
-types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
+type_synonym ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
       = "'a \<rightharpoonup> 'b"
-      ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
+type_synonym ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
       = "'a \<Rightarrow> 'b set"
 
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Term.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -57,7 +57,7 @@
 
 
 
-types locals = "(lname, val) table"  --{* local variables *}
+type_synonym locals = "(lname, val) table"  --{* local variables *}
 
 
 datatype jump
@@ -78,7 +78,7 @@
         | Jump jump   --{* break, continue, return *}
         | Error error -- {* runtime errors, we wan't to detect and proof absent
                             in welltyped programms *}
-types
+type_synonym
   abopt  = "abrupt option"
 
 text {* Local variable store and exception. 
@@ -235,7 +235,7 @@
 intermediate steps of class-initialisation.
 *}
  
-types "term" = "(expr+stmt,var,expr list) sum3"
+type_synonym "term" = "(expr+stmt,var,expr list) sum3"
 translations
   (type) "sig"   <= (type) "mname \<times> ty list"
   (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/Value.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -26,7 +26,7 @@
 primrec the_Addr :: "val \<Rightarrow> loc"
   where "the_Addr (Addr a) = a"
 
-types   dyn_ty      = "loc \<Rightarrow> ty option"
+type_synonym dyn_ty = "loc \<Rightarrow> ty option"
 
 primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
 where
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/Bali/WellType.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -28,7 +28,7 @@
 \end{itemize}
 *}
 
-types lenv
+type_synonym lenv
         = "(lname, ty) table"  --{* local variables, including This and Result*}
 
 record env = 
@@ -49,7 +49,7 @@
 
 section "Static overloading: maximally specific methods "
 
-types
+type_synonym
   emhead = "ref_ty \<times> mhead"
 
 --{* Some mnemotic selectors for emhead *}
@@ -244,7 +244,7 @@
 
 section "Typing for terms"
 
-types tys  = "ty + ty list"
+type_synonym tys  = "ty + ty list"
 translations
   (type) "tys" <= (type) "ty + ty list"
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/HOL/ZF/Games.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ZF/MainZF.thy/Games.thy
+(*  Title:      HOL/ZF/Games.thy
     Author:     Steven Obua
 
 An application of HOLZF: Partizan Games.  See "Partizan Games in
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Feb 18 17:05:19 2011 +0100
@@ -203,7 +203,7 @@
       Task_Queue.running task (fn () =>
         setmp_worker_task task (fn () =>
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
-    val _ = Multithreading.tracing 1 (fn () =>
+    val _ = Multithreading.tracing 2 (fn () =>
       let
         val s = Task_Queue.str_of_task task;
         fun micros time = string_of_int (Time.toNanoseconds time div 1000);
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/Pure/goal.ML	Fri Feb 18 17:05:19 2011 +0100
@@ -115,7 +115,7 @@
     let
       val n = m + i;
       val _ =
-        Multithreading.tracing 1 (fn () =>
+        Multithreading.tracing 2 (fn () =>
           ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
     in n end);
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/AC/AC17_AC1.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/AC/AC1_AC17.thy
+(*  Title:      ZF/AC/AC17_AC1.thy
     Author:     Krzysztof Grabczewski
 
 The equivalence of AC0, AC1 and AC17
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ArithSimp.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ArithSimp.ML
+(*  Title:      ZF/ArithSimp.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Bool.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/bool.thy
+(*  Title:      ZF/Bool.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Coind/Language.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -5,14 +5,14 @@
 
 theory Language imports Main begin
 
-consts
-  Const :: i                    (* Abstract type of constants *)
-  c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
-
 
 text{*these really can't be definitions without losing the abstraction*}
-axioms
-  constNEE:  "c \<in> Const ==> c \<noteq> 0"
+
+axiomatization
+  Const :: i  and               (* Abstract type of constants *)
+  c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
+where
+  constNEE:  "c \<in> Const ==> c \<noteq> 0" and
   c_appI:    "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
 
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/Coind/Static.thy
--- a/src/ZF/Coind/Static.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Coind/Static.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -9,11 +9,8 @@
      parameter of the proof.  A concrete version could be defined inductively.
 ***)
 
-consts
-  isof :: "[i,i] => o"
-
-axioms
-  isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
+axiomatization isof :: "[i,i] => o"
+  where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
 
 (*Its extension to environments*)
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Datatype_ZF.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Datatype.thy
+(*  Title:      ZF/Datatype_ZF.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Int_ZF.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Int.thy
+(*  Title:      ZF/Int_ZF.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/OrdQuant.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/AC/OrdQuant.thy
+(*  Title:      ZF/OrdQuant.thy
     Authors:    Krzysztof Grabczewski and L C Paulson
 *)
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/Sum.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/sum.thy
+(*  Title:      ZF/Sum.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/AllocBase.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -7,17 +7,16 @@
 
 theory AllocBase imports Follows MultisetSum Guar begin
 
-consts
-  NbT      :: i  (* Number of tokens in system *)
-  Nclients :: i  (* Number of clients *)
-
 abbreviation (input)
   tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
 where
   "tokbag == nat"
 
-axioms
-  NbT_pos:      "NbT \<in> nat-{0}"
+axiomatization
+  NbT :: i and  (* Number of tokens in system *)
+  Nclients :: i  (* Number of clients *)
+where
+  NbT_pos: "NbT \<in> nat-{0}" and
   Nclients_pos: "Nclients \<in> nat-{0}"
   
 text{*This function merely sums the elements of a list*}
@@ -27,9 +26,7 @@
   "tokens(Nil) = 0"
   "tokens (Cons(x,xs)) = x #+ tokens(xs)"
 
-consts
-  bag_of :: "i => i"
-
+consts bag_of :: "i => i"
 primrec
   "bag_of(Nil)    = 0"
   "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
@@ -38,7 +35,7 @@
 text{*Definitions needed in Client.thy.  We define a recursive predicate
 using 0 and 1 to code the truth values.*}
 consts all_distinct0 :: "i=>i"
- primrec
+primrec
   "all_distinct0(Nil) = 1"
   "all_distinct0(Cons(a, l)) =
      (if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -16,9 +16,9 @@
   available_tok :: i  (*number of free tokens (T in paper)*)  where
   "available_tok == Var([succ(succ(2))])"
 
-axioms
+axiomatization where
   alloc_type_assumes [simp]:
-  "type_of(NbR) = nat & type_of(available_tok)=nat"
+  "type_of(NbR) = nat & type_of(available_tok)=nat" and
 
   alloc_default_val_assumes [simp]:
   "default_val(NbR)  = 0 & default_val(available_tok)=0"
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -12,13 +12,13 @@
 abbreviation "rel == Var([1])" (* input history: tokens released *)
 abbreviation "tok == Var([2])" (* the number of available tokens *)
 
-axioms
+axiomatization where
   type_assumes:
   "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & 
-   type_of(rel) = list(tokbag) & type_of(tok) = nat"
+   type_of(rel) = list(tokbag) & type_of(tok) = nat" and
   default_val_assumes:
-  "default_val(ask) = Nil & default_val(giv)  = Nil & 
-   default_val(rel)  = Nil & default_val(tok)  = 0"
+  "default_val(ask) = Nil & default_val(giv) = Nil & 
+   default_val(rel) = Nil & default_val(tok) = 0"
 
 
 (*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/UNITY/Mutex.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -27,11 +27,11 @@
 abbreviation "u == Var([0,1])"
 abbreviation "v == Var([1,0])"
 
-axioms --{** Type declarations  **}
-  p_type:  "type_of(p)=bool & default_val(p)=0"
-  m_type:  "type_of(m)=int  & default_val(m)=#0"
-  n_type:  "type_of(n)=int  & default_val(n)=#0"
-  u_type:  "type_of(u)=bool & default_val(u)=0"
+axiomatization where --{** Type declarations  **}
+  p_type:  "type_of(p)=bool & default_val(p)=0" and
+  m_type:  "type_of(m)=int  & default_val(m)=#0" and
+  n_type:  "type_of(n)=int  & default_val(n)=#0" and
+  u_type:  "type_of(u)=bool & default_val(u)=0" and
   v_type:  "type_of(v)=bool & default_val(v)=0"
 
 definition
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ZF.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -207,21 +207,21 @@
   subset_def:    "A <= B == \<forall>x\<in>A. x\<in>B"
 
 
-axioms
+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 <= B & B <= A"
-  Union_iff:     "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)"
-  Pow_iff:       "A \<in> Pow(B) <-> A <= B"
+  extension:     "A = B <-> A <= B & B <= A" and
+  Union_iff:     "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and
+  Pow_iff:       "A \<in> Pow(B) <-> A <= B" and
 
   (*We may name this set, though it is not uniquely defined.*)
-  infinity:      "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)"
+  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~:A)"
+  foundation:    "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~: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) --> y=z) ==>
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ex/Commutation.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Lambda/Commutation.thy
+(*  Title:      ZF/ex/Commutation.thy
     Author:     Tobias Nipkow & Sidi Ould Ehmety
     Copyright   1995  TU Muenchen
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ex/LList.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -43,11 +43,9 @@
   lconst   :: "i => i"  where
   "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
-consts
-  flip     :: "i => i"
-axioms
-  flip_LNil:   "flip(LNil) = LNil"
-
+axiomatization flip :: "i => i"
+where
+  flip_LNil:   "flip(LNil) = LNil" and
   flip_LCons:  "[| x \<in> bool; l \<in> llist(bool) |] 
                 ==> flip(LCons(x,l)) = LCons(not(x), flip(l))"
 
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/ex/NatSum.thy
--- a/src/ZF/ex/NatSum.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/ex/NatSum.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/Natsum.thy
+(*  Title:      ZF/ex/NatSum.thy
     Author:     Tobias Nipkow & Lawrence C Paulson
 
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
diff -r 22d23da89aa5 -r 7eb9eac392b6 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Fri Feb 18 16:30:44 2011 +0100
+++ b/src/ZF/pair.thy	Fri Feb 18 17:05:19 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/pair
+(*  Title:      ZF/pair.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge