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/Lift_prog.thy
changeset 46911 6d2a2f0e904e
parent 46577 e5438c5797ae
child 58889 5b7a9633cfa8 
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -301,7 +301,7 @@
     "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
         F j \<in> preserves snd |]   
      ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
-apply (case_tac "i=j")
+apply (cases "i=j")
 apply (simp add: lift_def lift_set_def rename_constrains)
 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
        assumption)
isabelle