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/Bali/Conform.thy
changeset 63566 e5abbdee461a
parent 62042 6c6ccf573479
child 63648 f9f3006a5579 
--- a/src/HOL/Bali/Conform.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Bali/Conform.thy	Fri Jul 29 20:34:07 2016 +0200
@@ -519,9 +519,9 @@
 apply safe
 apply (rule lconf_upd)
 apply auto
-apply (simp only: obj_ty_cong) 
+apply (simp only: obj_ty_cong)
 apply (force dest: conforms_globsD intro!: lconf_upd 
-       simp add: oconf_def cong del: sum.case_cong_weak)
+       simp add: oconf_def cong del: old.sum.case_cong_weak)
 done
 
 lemma conforms_set_locals:
isabelle