# HG changeset patch
# User traytel
# Date 1377870863 -7200
# Node ID c97a05a26dd6be7425f562bbf4d32deff5dc2ff5
# Parent  20440c789759482dfe4765858ece2e5c0f935288
Doc improvements

diff -r 20440c789759 -r c97a05a26dd6 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:36:00 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:54:23 2013 +0200
@@ -246,10 +246,11 @@
 simplest recursive type: copy of the natural numbers:
 *}
 
+    datatype_new nat = Zero | Suc nat
 (*<*)
-    (* FIXME: remove "rep_compat" once "datatype_new" is integrated with "fun" *)
+    (* FIXME: remove once "datatype_new" is integrated with "fun" *)
+    datatype_new_compat nat
 (*>*)
-    datatype_new (*<*)(rep_compat) (*>*)nat = Zero | Suc nat
 
 text {*
 lists were shown in the introduction; terminated lists are a variant:
@@ -638,16 +639,12 @@
 we don't like the confusing name @{const nth}:
 *}
 
-    (* FIXME *)
-    primrec_new_notyet at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
+    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
       "at (a # as) j =
          (case j of
             Zero \<Rightarrow> a
           | Suc j' \<Rightarrow> at as j')"
 
-    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
-      "at (a # as) j = nat_case a (at as) j"
-
     primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
       "tfold _ (TNil b) = b" |
       "tfold f (TCons a as) = f a (tfold f as)"
@@ -674,11 +671,6 @@
 Mutual recursion is be possible within a single type, but currently only using fun:
 *}
 
-(*<*)
-    (* FIXME: remove hack once "primrec_new" is in place *)
-    rep_datatype Zero Suc
-    by (erule nat.induct, assumption) auto
-(*>*)
     fun
       even :: "nat \<Rightarrow> bool" and
       odd :: "nat \<Rightarrow> bool"