Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Bali/Basis.thy
changeset 58249 180f1b3508ed
parent 57983 6edc3529bb4e
child 58310 91ea607a34d8 
--- a/src/HOL/Bali/Basis.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Basis.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -155,7 +155,7 @@
 primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
   where "the_Inr (Inr b) = b"
 
-datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
+datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
 
 primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
   where "the_In1 (In1 a) = a"
isabelle