--- a/src/Doc/Tutorial/CTL/CTL.thy Wed Aug 29 12:07:45 2012 +0200
+++ b/src/Doc/Tutorial/CTL/CTL.thy Wed Aug 29 12:07:57 2012 +0200
@@ -399,7 +399,7 @@
definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
"eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"
-axioms
+axiomatization where
M_total: "\<exists>t. (s,t) \<in> M"
consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)"
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy Wed Aug 29 12:07:45 2012 +0200
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy Wed Aug 29 12:07:57 2012 +0200
@@ -132,8 +132,8 @@
function:
*};
-consts f :: "nat \<Rightarrow> nat";
-axioms f_ax: "f(f(n)) < f(Suc(n))";
+axiomatization f :: "nat \<Rightarrow> nat"
+ where f_ax: "f(f(n)) < f(Suc(n))"
text{*
\begin{warn}
--- a/src/Doc/Tutorial/Types/Typedefs.thy Wed Aug 29 12:07:45 2012 +0200
+++ b/src/Doc/Tutorial/Types/Typedefs.thy Wed Aug 29 12:07:57 2012 +0200
@@ -41,7 +41,7 @@
axioms. Example:
*}
-axioms
+axiomatization where
just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
text{*\noindent