author | paulson |
Sun, 03 Jan 2010 11:03:22 +0000 | |
changeset 34235 | 43bf58fdbace |
parent 34233 | 156c42518cfc (current diff) |
parent 34234 | 86a985e9b4df (diff) |
child 34236 | 010a3206cbbe |
--- a/src/HOL/UNITY/UNITY_tactics.ML Sun Jan 03 10:01:23 2010 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Sun Jan 03 11:03:22 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 =