Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Simple/Reach.thy
changeset 62390 842917225d56
parent 46911 6d2a2f0e904e
child 63146 f1ecba0272f9 
--- a/src/HOL/UNITY/Simple/Reach.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -45,7 +45,7 @@
     "[| if P then Q else R;     
         [| P;   Q |] ==> S;     
         [| ~ P; R |] ==> S |] ==> S"
-by (simp split: split_if_asm) 
+by (simp split: if_split_asm) 
 
 
 declare Rprg_def [THEN def_prg_Init, simp]
isabelle