--- a/src/HOL/Lex/AutoChopper1.thy Sat Mar 18 19:20:10 2000 +0100
+++ b/src/HOL/Lex/AutoChopper1.thy Mon Mar 20 10:23:24 2000 +0100
@@ -17,7 +17,7 @@
No proofs yet.
*)
-AutoChopper1 = DA + Chopper + Recdef +
+AutoChopper1 = DA + Chopper + Main +
consts
acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
@@ -25,7 +25,6 @@
recdef acc "inv_image (less_than ** less_than)
(%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
length ys))"
-simpset "simpset() addsimps (less_add_Suc2::add_ac)"
"acc(A,[],s,xss,zs,[]) = (xss, zs)"
"acc(A,[],s,xss,zs,x#xs) = acc(A,zs,start A, xss @ [x#xs],[],[])"
"acc(A,y#ys,s,xss,zs,xs) =
--- a/src/HOL/ex/Recdefs.thy Sat Mar 18 19:20:10 2000 +0100
+++ b/src/HOL/ex/Recdefs.thy Mon Mar 20 10:23:24 2000 +0100
@@ -36,7 +36,6 @@
consts gcd :: "nat * nat => nat"
recdef gcd "measure (%(x,y).x+y)"
- simpset "simpset() addsimps [less_Suc_eq_le, 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)