# HG changeset patch # User nipkow # Date 761303117 -3600 # Node ID 64eda8afe2b418dd943780481c00ab67077d4c90 # Parent 424c7b1489df800db19e39c01b46acde9c0d3c71 deleted duplicate rewrite rules diff -r 424c7b1489df -r 64eda8afe2b4 LList.ML --- a/LList.ML Tue Feb 15 07:55:22 1994 +0100 +++ b/LList.ML Tue Feb 15 10:05:17 1994 +0100 @@ -16,7 +16,6 @@ val llist_simps = [sum_case_Inl, sum_case_Inr]; val llist_ss = univ_ss delsimps [Pair_eq] - addsimps llist_simps addcongs [split_weak_cong, sum_case_weak_cong] setloop (split_tac [expand_split, expand_sum_case]); @@ -155,8 +154,8 @@ by (stac LList_corec 1); (*nested "sum_case"; requires an explicit split*) by (res_inst_tac [("s", "f(xa)")] sumE 1); -by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_NIL_I])) 1); -by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_CONS_I, range_eqI]) +by (asm_simp_tac (univ_ss addsimps [List_Fun_NIL_I]) 1); +by (asm_simp_tac (univ_ss addsimps [List_Fun_CONS_I, range_eqI] setloop (split_tac [expand_split])) 1); (* FIXME: can the selection of the case split be automated? by (ASM_SIMP_TAC (llist_ss addsimps [List_Fun_CONS_I, rangeI]) 1);*) diff -r 424c7b1489df -r 64eda8afe2b4 List.ML --- a/List.ML Tue Feb 15 07:55:22 1994 +0100 +++ b/List.ML Tue Feb 15 10:05:17 1994 +0100 @@ -395,7 +395,7 @@ "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \ \ (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (list_ss addsimps [list_case_Nil,list_case_Cons]))); +by(ALLGOALS(asm_simp_tac list_ss)); by(fast_tac HOL_cs 1); val expand_list_case = result(); diff -r 424c7b1489df -r 64eda8afe2b4 ex/Qsort.ML --- a/ex/Qsort.ML Tue Feb 15 07:55:22 1994 +0100 +++ b/ex/Qsort.ML Tue Feb 15 10:05:17 1994 +0100 @@ -84,11 +84,6 @@ Qsort.qsort_Nil,Qsort.qsort_Cons]; -goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; -by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); -val ss = ss addsimps [result()]; - goal Qsort.thy "x mem qsort(le,xs) = x mem xs"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); diff -r 424c7b1489df -r 64eda8afe2b4 ex/qsort.ML --- a/ex/qsort.ML Tue Feb 15 07:55:22 1994 +0100 +++ b/ex/qsort.ML Tue Feb 15 10:05:17 1994 +0100 @@ -84,11 +84,6 @@ Qsort.qsort_Nil,Qsort.qsort_Cons]; -goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; -by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); -val ss = ss addsimps [result()]; - goal Qsort.thy "x mem qsort(le,xs) = x mem xs"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); diff -r 424c7b1489df -r 64eda8afe2b4 llist.ML --- a/llist.ML Tue Feb 15 07:55:22 1994 +0100 +++ b/llist.ML Tue Feb 15 10:05:17 1994 +0100 @@ -16,7 +16,6 @@ val llist_simps = [sum_case_Inl, sum_case_Inr]; val llist_ss = univ_ss delsimps [Pair_eq] - addsimps llist_simps addcongs [split_weak_cong, sum_case_weak_cong] setloop (split_tac [expand_split, expand_sum_case]); @@ -155,8 +154,8 @@ by (stac LList_corec 1); (*nested "sum_case"; requires an explicit split*) by (res_inst_tac [("s", "f(xa)")] sumE 1); -by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_NIL_I])) 1); -by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_CONS_I, range_eqI]) +by (asm_simp_tac (univ_ss addsimps [List_Fun_NIL_I]) 1); +by (asm_simp_tac (univ_ss addsimps [List_Fun_CONS_I, range_eqI] setloop (split_tac [expand_split])) 1); (* FIXME: can the selection of the case split be automated? by (ASM_SIMP_TAC (llist_ss addsimps [List_Fun_CONS_I, rangeI]) 1);*)