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/IMP/Abs_Int2.thy
changeset 73932 fd21b4a93043
parent 69712 dc85b5b3a532 
--- a/src/HOL/IMP/Abs_Int2.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -65,7 +65,7 @@
 
 lemma in_gamma_sup_UpI:
   "s \<in> \<gamma>\<^sub>o S1 \<or> s \<in> \<gamma>\<^sub>o S2 \<Longrightarrow> s \<in> \<gamma>\<^sub>o(S1 \<squnion> S2)"
-by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
+by (metis (opaque_lifting, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
 
 fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
 "aval'' e None = \<bottom>" |
isabelle