Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed expand_split from simpset.
authornipkow
Tue, 10 Mar 1998 13:23:35 +0100
changeset 4712 facfbbca7242
parent 4711 75a9ef36b1fe
child 4713 bea2ab2e360b
Removed expand_split from simpset.
src/HOL/Lex/AutoChopper1.thy file | annotate | diff | comparison | revisions
src/HOL/Lex/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lex/AutoChopper1.thy	Mon Mar 09 16:30:55 1998 +0100
+++ b/src/HOL/Lex/AutoChopper1.thy	Tue Mar 10 13:23:35 1998 +0100
@@ -25,7 +25,7 @@
 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) addsplits [expand_if]"
+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/Lex/ROOT.ML	Mon Mar 09 16:30:55 1998 +0100
+++ b/src/HOL/Lex/ROOT.ML	Tue Mar 10 13:23:35 1998 +0100
@@ -8,4 +8,5 @@
 
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
+use_thy"AutoMaxChop";
 use_thy"Regset_of_auto";
isabelle