--- 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
--- 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
--- 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
--- 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)"
--- 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 *}
--- 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"
--- 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"
--- 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"
--- 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