# HG changeset patch
# User wenzelm
# Date 1346234877 -7200
# Node ID c84278efa9d5073d15fce3a5ddb01acbc10dcfe3
# Parent  44428ea53dc17ad48bef029449488b1c958cffc3
modernized specifications;

diff -r 44428ea53dc1 -r c84278efa9d5 src/Doc/Tutorial/CTL/CTL.thy
--- 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)"
diff -r 44428ea53dc1 -r c84278efa9d5 src/Doc/Tutorial/Misc/AdvancedInd.thy
--- 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}
diff -r 44428ea53dc1 -r c84278efa9d5 src/Doc/Tutorial/Types/Typedefs.thy
--- 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