Mercurial Mercurial > hg > nominal2 / 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.
Nominal/Ex/SFT/Theorem.thy
changeset 3088 5e74bd87bcda
parent 3087 c95afd0dc594
child 3175 52730e5ec8cb 
--- a/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -55,7 +55,7 @@
   fixes F :: lam
   shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>"
 proof -
-  obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
+  obtain x :: name where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
   def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))"
   def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>"
   have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def ..
nominal2