updated mini_ss
authoroheimb
Sat Feb 15 17:44:10 1997 +0100 (1997-02-15)
changeset 2634b85c77b64c7a
parent 2633 37c0b5a7ee5d
child 2635 835820c1591d
updated mini_ss
src/FOL/ex/mini.ML
     1.1 --- a/src/FOL/ex/mini.ML	Sat Feb 15 17:43:27 1997 +0100
     1.2 +++ b/src/FOL/ex/mini.ML	Sat Feb 15 17:44:10 1997 +0100
     1.3 @@ -60,14 +60,7 @@
     1.4                   "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
     1.5  
     1.6  
     1.7 -val mini_ss = 
     1.8 -  empty_ss 
     1.9 -  setmksimps (map mk_meta_eq o atomize o gen_all)
    1.10 -  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
    1.11 -                          ORELSE' assume_tac
    1.12 -                          ORELSE' etac FalseE)
    1.13 -  setsubgoaler asm_simp_tac
    1.14 -  addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
    1.15 +val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
    1.16  
    1.17  val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss;
    1.18