--- a/src/HOL/ex/Recdef.thy Mon Nov 03 14:09:16 1997 +0100
+++ b/src/HOL/ex/Recdef.thy Mon Nov 03 14:37:35 1997 +0100
@@ -31,7 +31,7 @@
consts qsort ::"('a => 'a => bool) * 'a list => 'a list"
recdef qsort "measure (size o snd)"
- simpset "!simpset addsimps [le_eq_less_Suc RS sym, filter_size]"
+ simpset "simpset() addsimps [le_eq_less_Suc RS sym, filter_size]"
"qsort(ord, []) = []"
"qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)
@ [x] @
@@ -44,7 +44,7 @@
consts gcd :: "nat * nat => nat"
recdef gcd "measure (%(x,y).x+y)"
- simpset "!simpset addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
+ simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
"gcd (0,y) = y"
"gcd (Suc x, 0) = Suc x"
"gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)