--- a/src/ZF/Arith.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/Arith.ML Tue Sep 22 13:50:57 1998 +0200
@@ -123,7 +123,7 @@
by (rtac (prems MRS diff_induct) 1);
by (etac leE 3);
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps (prems @ [le_iff, nat_into_Ord]))));
+ (asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord])));
qed "diff_le_self";
(*** Simplification over add, mult, diff ***)
--- a/src/ZF/CardinalArith.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/CardinalArith.ML Tue Sep 22 13:50:57 1998 +0200
@@ -708,7 +708,7 @@
Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
by (etac nat_induct 1);
-by (simp_tac (simpset() addsimps (eqpoll_0_iff::Fin.intrs)) 1);
+by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
by (Clarify_tac 1);
by (subgoal_tac "EX u. u:A" 1);
by (etac exE 1);
--- a/src/ZF/Coind/Types.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/Coind/Types.ML Tue Sep 22 13:50:57 1998 +0200
@@ -15,13 +15,13 @@
Goal "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp";
by (rtac (te_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
+by (simp_tac (simpset() addsimps rank_te_owr1::TyEnv.case_eqns) 1);
qed "te_rec_emp";
Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
\ f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
by (rtac (te_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
+by (simp_tac (rank_ss addsimps rank_te_owr1::TyEnv.case_eqns) 1);
qed "te_rec_owr";
Goalw [te_dom_def] "te_dom(te_emp) = 0";
--- a/src/ZF/List.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/List.ML Tue Sep 22 13:50:57 1998 +0200
@@ -61,7 +61,7 @@
\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \
\ |] ==> list_case(c,h,l) : C(l)";
by (rtac (major RS list.induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (list.case_eqns @ prems))));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps list.case_eqns @ prems)));
qed "list_case_type";
@@ -135,7 +135,7 @@
Goal "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps (rank_Cons2::list.case_eqns)) 1);
+by (simp_tac (rank_ss addsimps rank_Cons2::list.case_eqns) 1);
qed "list_rec_Cons";
Addsimps [list_rec_Nil, list_rec_Cons];
--- a/src/ZF/Nat.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/Nat.ML Tue Sep 22 13:50:57 1998 +0200
@@ -142,7 +142,7 @@
by (nat_ind_tac "n" prems 1);
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps (prems@distrib_simps@[le0_iff, le_succ_iff]))));
+ (simpset() addsimps prems @ distrib_simps @ [le0_iff, le_succ_iff])));
qed "nat_induct_from_lemma";
(*Induction starting from m rather than 0*)
--- a/src/ZF/OrdQuant.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/OrdQuant.ML Tue Sep 22 13:50:57 1998 +0200
@@ -88,7 +88,7 @@
"[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
(fn prems=>
[ rtac equality_iffI 1,
- simp_tac (simpset() addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]);
+ simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1 ]);
AddSIs [oallI];
AddIs [oexI, OUN_I];
--- a/src/ZF/OrderType.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/OrderType.ML Tue Sep 22 13:50:57 1998 +0200
@@ -793,7 +793,7 @@
val prems =
Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \
\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
-by (asm_simp_tac (simpset() addsimps (prems@[Ord_UN, omult_unfold])) 1);
+by (asm_simp_tac (simpset() addsimps prems @ [Ord_UN, omult_unfold]) 1);
by (Blast_tac 1);
qed "omult_UN";
--- a/src/ZF/Perm.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/Perm.ML Tue Sep 22 13:50:57 1998 +0200
@@ -39,7 +39,7 @@
\ !!y. y:B ==> c(d(y)) = y \
\ |] ==> (lam x:A. c(x)) : surj(A,B)";
by (res_inst_tac [("d", "d")] f_imp_surjective 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps ([lam_type]@prems)) ));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems) ));
qed "lam_surjective";
(*Cantor's theorem revisited*)
@@ -79,7 +79,7 @@
\ !!x. x:A ==> d(c(x)) = x \
\ |] ==> (lam x:A. c(x)) : inj(A,B)";
by (res_inst_tac [("d", "d")] f_imp_injective 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps ([lam_type]@prems)) ));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems)));
qed "lam_injective";
(** Bijections **)
--- a/src/ZF/ROOT.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/ROOT.ML Tue Sep 22 13:50:57 1998 +0200
@@ -38,9 +38,15 @@
use "typechk.ML";
use_thy "InfDatatype";
use_thy "List";
-use_thy "EquivClass";
-(*printing functions are inherited from FOL*)
+(*Integers & binary integer arithmetic*)
+cd "Integ";
+use_thy "Bin";
+cd "..";
+
+(*the all-in-one theory*)
+use_thy "Main";
+
print_depth 8;
Goal "True"; (*leave subgoal package empty*)
--- a/src/ZF/ex/LList.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/ex/LList.ML Tue Sep 22 13:50:57 1998 +0200
@@ -160,7 +160,7 @@
by (etac llist.elim 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps ([QInl_def,QInr_def]@llist.con_defs))));
+ (asm_simp_tac (simpset() addsimps [QInl_def,QInr_def] @ llist.con_defs)));
(*LCons case*)
by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
qed "flip_llist_quniv_lemma";
--- a/src/ZF/ex/Limit.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/ex/Limit.ML Tue Sep 22 13:50:57 1998 +0200
@@ -1530,7 +1530,7 @@
val prems = goal Limit.thy (* e_less_succ_emb *)
"[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==> \
\ e_less(DD,ee,m,succ(m)) = ee`m";
-by (asm_simp_tac(simpset() addsimps(e_less_succ::prems)) 1);
+by (asm_simp_tac(simpset() addsimps e_less_succ::prems) 1);
by (stac comp_id 1);
brr(emb_cont::cont_fun::refl::prems) 1;
qed "e_less_succ_emb";
@@ -1822,15 +1822,15 @@
val prems = goal Limit.thy (* eps_succ_ee *)
"[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==> \
\ eps(DD,ee,m,succ(m)) = ee`m";
-by (asm_simp_tac(simpset() addsimps(eps_e_less::le_succ_iff::e_less_succ_emb::
- prems)) 1);
+by (asm_simp_tac(simpset() addsimps eps_e_less::le_succ_iff::e_less_succ_emb::
+ prems) 1);
qed "eps_succ_ee";
Goal (* eps_succ_Rp *)
"[|emb_chain(DD,ee); m:nat|] ==> \
\ eps(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)";
-by (asm_simp_tac(simpset() addsimps(eps_e_gr::le_succ_iff::e_gr_succ_emb::
- prems)) 1);
+by (asm_simp_tac(simpset() addsimps eps_e_gr::le_succ_iff::e_gr_succ_emb::
+ prems) 1);
qed "eps_succ_Rp";
Goal (* eps_cont *)
--- a/src/ZF/indrule.ML Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/indrule.ML Tue Sep 22 13:50:57 1998 +0200
@@ -226,7 +226,7 @@
(*some risk of excessive simplification here -- might have
to identify the bare minimum set of rewrites*)
full_simp_tac
- (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
+ (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1) THEN