# HG changeset patch
# User paulson
# Date 953544204 -3600
# Node ID 581dfabf22dde9391c8192372b6dd31e5263538e
# Parent  4e42e1734004ee40b89bfeb906e86a3a7a2b8929
deleted unnecessary "simpset" part from recdef

diff -r 4e42e1734004 -r 581dfabf22dd src/HOL/Lex/AutoChopper1.thy
--- 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) =
diff -r 4e42e1734004 -r 581dfabf22dd src/HOL/ex/Recdefs.thy
--- 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)