--- a/src/Doc/Functions/Functions.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Functions/Functions.thy Thu Sep 11 19:32:36 2014 +0200
@@ -522,7 +522,7 @@
and @{term "X"} for true, false and uncertain propositions, respectively.
*}
-datatype_new P3 = T | F | X
+datatype P3 = T | F | X
text {* \noindent Then the conjunction of such values can be defined as follows: *}
@@ -1122,7 +1122,7 @@
As an example, imagine a datatype of n-ary trees:
*}
-datatype_new 'a tree =
+datatype 'a tree =
Leaf 'a
| Branch "'a tree list"