Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned the eqvt-proof
authorurbanc
Wed, 11 Jan 2006 14:00:11 +0100
changeset 18653 7a00c80400b1
parent 18652 3930a060d71b
child 18654 94782c7c4247
tuned the eqvt-proof
src/HOL/Nominal/Examples/Weakening.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 12:21:01 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 14:00:11 2006 +0100
@@ -42,7 +42,7 @@
   shows   "valid (pi\<bullet>\<Gamma>)"
 using a
 apply(induct)
-apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+apply(auto simp add: fresh_eqvt)
 done
 
 (* typing judgements *)
isabelle