Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorpaulson
Sun, 03 Jan 2010 11:03:22 +0000
changeset 34235 43bf58fdbace
parent 34233 156c42518cfc (current diff)
parent 34234 86a985e9b4df (diff)
child 34236 010a3206cbbe
merged
--- 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 =
isabelle