# HG changeset patch
# User wenzelm
# Date 1332190329 -3600
# Node ID 36dacca8a95cc173a5cf1e4d9dd20bc034dc1686
# Parent  b2b8ae61d6ad6d80f612c4cb0f7500a82ecb6167
modernized axiomatizations;

diff -r b2b8ae61d6ad -r 36dacca8a95c src/HOL/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Mar 19 21:49:52 2012 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Mar 19 21:52:09 2012 +0100
@@ -19,25 +19,25 @@
   countm :: "['a multiset, 'a => bool] => nat"
   count  :: "['a multiset, 'a] => nat"
 
-axioms
+axiomatization where
 
 delm_empty_def:
-  "delm {|} x = {|}"
+  "delm {|} x = {|}" and
 
 delm_nonempty_def:
-  "delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
+  "delm (addm M x) y == (if x=y then M else addm (delm M y) x)" and
 
 countm_empty_def:
-   "countm {|} P == 0"
+   "countm {|} P == 0" and
 
 countm_nonempty_def:
-   "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
+   "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" and
 
 count_def:
-   "count M x == countm M (%y. y = x)"
+   "count M x == countm M (%y. y = x)" and
 
 "induction":
-   "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
+   "\<And>P M. [| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
 
 lemma count_empty: 
    "count {|} x = 0"
diff -r b2b8ae61d6ad -r 36dacca8a95c src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Mon Mar 19 21:49:52 2012 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Mon Mar 19 21:52:09 2012 +0100
@@ -61,7 +61,7 @@
         Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
         asig_comp sigA sigB)"
 
-axioms
+axiomatization where
 
 finiteR_mksch:
   "Finite (mksch A B$tr$x$y) --> Finite tr"
diff -r b2b8ae61d6ad -r 36dacca8a95c src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Mon Mar 19 21:49:52 2012 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Mon Mar 19 21:52:09 2012 +0100
@@ -78,13 +78,13 @@
   "validIOA A P == ! ex : executions A . (ex |== P)"
 
 
-axioms
+axiomatization where
 
 mkfin_UU:
-  "mkfin UU = nil"
+  "mkfin UU = nil" and
 
 mkfin_nil:
-  "mkfin nil =nil"
+  "mkfin nil =nil" and
 
 mkfin_cons:
   "(mkfin (a>>s)) = (a>>(mkfin s))"