Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new primrec
authorhaftmann
Fri, 07 Dec 2007 15:08:07 +0100
changeset 25572 0c9052719f20
parent 25571 c9e39eafc7a0
child 25573 a0e695567236
new primrec
src/HOL/ex/ExecutableContent.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/ExecutableContent.thy	Fri Dec 07 15:07:59 2007 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Fri Dec 07 15:08:07 2007 +0100
@@ -39,15 +39,14 @@
 datatype mut1 = Tip | Top mut2
   and mut2 = Tip | Top mut1
 
-consts
+primrec
   mut1 :: "mut1 \<Rightarrow> mut1"
-  mut2 :: "mut2 \<Rightarrow> mut2"
-
-primrec
+  and mut2 :: "mut2 \<Rightarrow> mut2"
+where
   "mut1 mut1.Tip = mut1.Tip"
-  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
-  "mut2 mut2.Tip = mut2.Tip"
-  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
+  | "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
+  | "mut2 mut2.Tip = mut2.Tip"
+  | "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
 
 definition
   "mystring = ''my home is my castle''"
isabelle