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/Basic_BNF_LFPs.thy
changeset 69850 5f993636ac07
parent 69605 a96320074298 
--- a/src/HOL/Basic_BNF_LFPs.thy	Thu Feb 28 21:37:24 2019 +0100
+++ b/src/HOL/Basic_BNF_LFPs.thy	Thu Feb 28 21:59:58 2019 +0100
@@ -84,12 +84,12 @@
 lemma map_sum_sel:
   "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
   "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
-  by (case_tac [!] s) simp_all
+  by (cases s; simp)+
 
 lemma set_sum_sel:
   "isl s \<Longrightarrow> projl s \<in> setl s"
   "\<not> isl s \<Longrightarrow> projr s \<in> setr s"
-  by (case_tac [!] s) (auto intro: setl.intros setr.intros)
+  by (cases s; auto intro: setl.intros setr.intros)+
 
 lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
   (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
isabelle