--- a/src/Doc/Isar_Ref/Spec.thy Thu Sep 11 19:45:42 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Sep 11 19:59:46 2014 +0200
@@ -81,7 +81,7 @@
the formal text. Examples may be seen in Isabelle/HOL sources
itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
@{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
- "\"old_datatype\""} @{text ":: thy_decl"} for theory-level declarations
+ "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 19:45:42 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 19:59:46 2014 +0200
@@ -37,7 +37,7 @@
and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-old_datatype 'a up = bot | Up 'a
+datatype 'a up = bot | Up 'a
instantiation up :: (SL_top)SL_top
begin