# HG changeset patch # User wenzelm # Date 937927602 -7200 # Node ID 08b2d5c94b8a376bf46f5b3012a50d92f08c948a # Parent 1b977741f5302c87f796a4e715640f4422b63f3d setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts; eliminated asm_simp; tuned improper methods; diff -r 1b977741f530 -r 08b2d5c94b8a src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Tue Sep 21 17:24:50 1999 +0200 +++ b/src/Provers/simplifier.ML Tue Sep 21 17:26:42 1999 +0200 @@ -417,7 +417,6 @@ (* add / del *) val simpN = "simp"; -val asm_simpN = "asm_simp"; val addN = "add"; val delN = "del"; val onlyN = "only"; @@ -468,29 +467,21 @@ Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local), Args.$$$ otherN >> K (I, I)]; -val simp_args = Method.only_sectioned_args simp_modifiers'; - -fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts => - FIRSTGOAL - ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac) - THEN' (if cut then Method.insert_tac facts else K all_tac) - THEN' tac (get_local_simpset ctxt))); - -val simp_method = simp_args ooo simp_meth; +fun simp_method tac = + (fn prems => fn ctxt => Method.METHOD (fn facts => + FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) + |> Method.bang_sectioned_args simp_modifiers'; (* setup_methods *) val setup_methods = Method.add_methods - [(simpN, simp_method true true (CHANGED oo asm_full_simp_tac), - "full simplification (including facts, excluding assumptions)"), - (asm_simpN, simp_method false true (CHANGED oo asm_full_simp_tac), - "full simplification (including facts and assumptions)"), - ("simp_tac", simp_method false false simp_tac, "simp_tac (improper!)"), - ("asm_simp_tac", simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"), - ("full_simp_tac", simp_method false false full_simp_tac, "full_simp_tac (improper!)"), - ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"), - ("asm_lr_simp_tac", simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")]; + [(simpN, simp_method (CHANGED oo asm_full_simp_tac), "full simplification"), + ("simp_tac", simp_method simp_tac, "simp_tac (improper!)"), + ("asm_simp_tac", simp_method asm_simp_tac, "asm_simp_tac (improper!)"), + ("full_simp_tac", simp_method full_simp_tac, "full_simp_tac (improper!)"), + ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"), + ("asm_lr_simp_tac", simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];