merged in lost update;
authorwenzelm
Tue Sep 21 23:06:50 1999 +0200 (1999-09-21 ago)
changeset 757144e9db3150f6
parent 7570 a9391550eea1
child 7572 6e6dafacbc28
merged in lost update;
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Tue Sep 21 19:11:07 1999 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Tue Sep 21 23:06:50 1999 +0200
     1.3 @@ -436,7 +436,6 @@
     1.4  (* add / del *)
     1.5  
     1.6  val simpN = "simp";
     1.7 -val asm_simpN = "asm_simp";
     1.8  val addN = "add";
     1.9  val delN = "del";
    1.10  val onlyN = "only";
    1.11 @@ -487,14 +486,6 @@
    1.12    Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
    1.13    Args.$$$ otherN >> K (I, I)];
    1.14  
    1.15 -val simp_args = Method.only_sectioned_args simp_modifiers';
    1.16 -
    1.17 -fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts =>
    1.18 -  FIRSTGOAL
    1.19 -    ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac)
    1.20 -      THEN' (if cut then Method.insert_tac facts else K all_tac)
    1.21 -      THEN' tac (get_local_simpset ctxt)));
    1.22 -
    1.23  fun simp_method tac =
    1.24    (fn prems => fn ctxt => Method.METHOD (fn facts =>
    1.25      FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
    1.26 @@ -504,15 +495,12 @@
    1.27  (* setup_methods *)
    1.28  
    1.29  val setup_methods = Method.add_methods
    1.30 - [(simpN,               simp_method true true (CHANGED oo asm_full_simp_tac),
    1.31 -    "full simplification (including facts, excluding assumptions)"),
    1.32 -  (asm_simpN,           simp_method false true (CHANGED oo asm_full_simp_tac),
    1.33 -    "full simplification (including facts and assumptions)"),
    1.34 -  ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
    1.35 -  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
    1.36 -  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),
    1.37 -  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
    1.38 -  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
    1.39 + [(simpN,               simp_method (CHANGED oo asm_full_simp_tac), "full simplification"),
    1.40 +  ("simp_tac",          simp_method simp_tac, "simp_tac (improper!)"),
    1.41 +  ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac (improper!)"),
    1.42 +  ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac (improper!)"),
    1.43 +  ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
    1.44 +  ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
    1.45  
    1.46  
    1.47