| changeset 66248 | df85956228c2 |
| parent 64413 | c0d5e78eb647 |
| child 67091 | 1393c2340eec |
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jul 03 09:57:26 2017 +0200 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jul 03 13:51:55 2017 +0200 @@ -17,7 +17,7 @@ "primcorec" :: thy_decl begin -setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close> +alias proj = Equiv_Relations.proj lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by simp