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/Nominal/Examples/Crary.thy
changeset 53374 a14d2a854c02
parent 53015 a1119cf551e8
child 63167 0909deb8059b 
--- a/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -766,9 +766,8 @@
   assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
   shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" 
 proof -
-  have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact
-  moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
-  ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
+  from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
+  with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
 qed
 
 lemma logical_subst_monotonicity :
isabelle