# HG changeset patch # User paulson # Date 1262516580 0 # Node ID 86a985e9b4df0f4927b8b49ae53376e4fd0cb124 # Parent ada8eb23a08ea71836b0e6eff318ce1ba61ed10e removed legacy asm_lr_simp_tac diff -r ada8eb23a08e -r 86a985e9b4df src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Thu Dec 31 23:47:09 2009 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Sun Jan 03 11:03:00 2010 +0000 @@ -29,7 +29,7 @@ full_simp_tac ss 1, REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS (clarify_tac cs), - ALLGOALS (asm_lr_simp_tac ss)]) i; + ALLGOALS (asm_full_simp_tac ss)]) i; (*proves "ensures/leadsTo" properties when the program is specified*) fun ensures_tac(cs,ss) sact =