# HG changeset patch
# User krauss
# Date 1174489575 -3600
# Node ID 43545e640877272c41115e7a275a4200a6640377
# Parent  535fbed859da752b032157daaffb3e41fc5e61d4
Unified function syntax

diff -r 535fbed859da -r 43545e640877 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -34,9 +34,9 @@
 fun
   add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where
   "add_sign (True, n) (True, m) = (True, n + m)"
-  "add_sign (False, n) (False, m) = (False, n + m)"
-  "add_sign (True, n) (False, m) = minus_sign n m"
-  "add_sign (False, n) (True, m) = minus_sign m n"
+| "add_sign (False, n) (False, m) = (False, n + m)"
+| "add_sign (True, n) (False, m) = minus_sign n m"
+| "add_sign (False, n) (True, m) = minus_sign m n"
 
 definition
   erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
diff -r 535fbed859da -r 43545e640877 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -64,7 +64,7 @@
 fun
   drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "drop_first f [] = []"
-  "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
+| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
 declare drop_first.simps [code del]
 declare drop_first.simps [code target: List]
 
@@ -150,7 +150,7 @@
 function unions :: "'a list list \<Rightarrow> 'a list"
 where
   "unions [] = []"
-  "unions xs = foldr unionl xs []"
+| "unions xs = foldr unionl xs []"
 by pat_completeness auto
 termination by lexicographic_order
 
diff -r 535fbed859da -r 43545e640877 src/HOL/Library/SCT_Examples.thy
--- a/src/HOL/Library/SCT_Examples.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Library/SCT_Examples.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -47,9 +47,9 @@
 function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 where
   "foo True (Suc n) m = foo True n (Suc m)"
-  "foo True 0 m = foo False 0 m"
-  "foo False n (Suc m) = foo False (Suc n) m"
-  "foo False n 0 = n"
+| "foo True 0 m = foo False 0 m"
+| "foo False n (Suc m) = foo False (Suc n) m"
+| "foo False n 0 = n"
 by pat_completeness auto
 
 termination
diff -r 535fbed859da -r 43545e640877 src/HOL/Library/SCT_Interpretation.thy
--- a/src/HOL/Library/SCT_Interpretation.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Library/SCT_Interpretation.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -65,7 +65,7 @@
 fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
   "mk_rel [] x y = False"
-  "mk_rel (c#cs) x y =
+| "mk_rel (c#cs) x y =
   (in_cdesc c x y \<or> mk_rel cs x y)"
 
 
diff -r 535fbed859da -r 43545e640877 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Library/State_Monad.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -257,12 +257,12 @@
 fun
   list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   "list f [] = id"
-  "list f (x#xs) = (do f x; list f xs done)"
+| "list f (x#xs) = (do f x; list f xs done)"
 lemmas [code] = list.simps
 
 fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
   "list_yield f [] = return []"
-  "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
+| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
 lemmas [code] = list_yield.simps
   
 text {* combinator properties *}
diff -r 535fbed859da -r 43545e640877 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -340,7 +340,7 @@
   lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm"   
 where
   "lookup [] X        = Var X"
-  "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
+| "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"name prm"
diff -r 535fbed859da -r 43545e640877 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -90,7 +90,7 @@
   lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"   
 where
   "lookup [] x        = Var x"
-  "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
+| "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"name prm"
diff -r 535fbed859da -r 43545e640877 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -11,8 +11,8 @@
 fun
   abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   "abs_sorted cmp [] \<longleftrightarrow> True"
-  "abs_sorted cmp [x] \<longleftrightarrow> True"
-  "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"
+| "abs_sorted cmp [x] \<longleftrightarrow> True"
+| "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"
 
 abbreviation (in ord)
   "sorted \<equiv> abs_sorted less_eq"
@@ -105,7 +105,7 @@
   product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
   where
   "product [] ys = []"
-  "product (x#xs) ys = map (Pair x) ys @ product xs ys"
+| "product (x#xs) ys = map (Pair x) ys @ product xs ys"
 
 lemma product_all:
   assumes "x \<in> set xs" "y \<in> set ys"
diff -r 535fbed859da -r 43545e640877 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/ex/Fundefs.thy	Wed Mar 21 16:06:15 2007 +0100
@@ -114,9 +114,9 @@
 function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
   "gcd3 x 0 = x"
-  "gcd3 0 y = y"
-  "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
-  "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
+| "gcd3 0 y = y"
+| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
+| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
   apply (case_tac x, case_tac a, auto)
   apply (case_tac ba, auto)
   done
@@ -131,7 +131,7 @@
 function ev :: "nat \<Rightarrow> bool"
 where
   "ev (2 * n) = True"
-  "ev (2 * n + 1) = False"
+| "ev (2 * n + 1) = False"
 proof -  -- {* completeness is more difficult here \dots *}
   fix P :: bool
     and x :: nat