removed legacy asm_lr_simp_tac
authorpaulson
Sun Jan 03 11:03:00 2010 +0000 (2010-01-03)
changeset 3423486a985e9b4df
parent 34216 ada8eb23a08e
child 34235 43bf58fdbace
removed legacy asm_lr_simp_tac
src/HOL/UNITY/UNITY_tactics.ML
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Dec 31 23:47:09 2009 +0100
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Sun Jan 03 11:03:00 2010 +0000
     1.3 @@ -29,7 +29,7 @@
     1.4                full_simp_tac ss 1,
     1.5                REPEAT (FIRSTGOAL (etac disjE)),
     1.6                ALLGOALS (clarify_tac cs),
     1.7 -              ALLGOALS (asm_lr_simp_tac ss)]) i;
     1.8 +              ALLGOALS (asm_full_simp_tac ss)]) i;
     1.9  
    1.10  (*proves "ensures/leadsTo" properties when the program is specified*)
    1.11  fun ensures_tac(cs,ss) sact =