--- 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);*)
--- 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();
--- 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]))));
--- 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]))));
--- 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);*)