--- 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"
--- 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"
--- 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))"