# HG changeset patch
# User paulson
# Date 906465057 -7200
# Node ID 4a54acae6a159e2639c6197e772fe918d4fe7721
# Parent  4896b4e4077b4aff0264a5472bbfa9563887a9a4
tidying

diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/Arith.ML
--- 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 ***)
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/CardinalArith.ML
--- 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);
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/Coind/Types.ML
--- 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";
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/List.ML
--- 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];
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/Nat.ML
--- 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*)
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/OrdQuant.ML
--- 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];
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/OrderType.ML
--- 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";
 
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/Perm.ML
--- 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 **)
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/ROOT.ML
--- 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*)
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/ex/LList.ML
--- 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";
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/ex/Limit.ML
--- 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 *)
diff -r 4896b4e4077b -r 4a54acae6a15 src/ZF/indrule.ML
--- 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