src/HOL/Nominal/Examples/Class.thy

 
 lemma a_starI:
   assumes a: "M \<longrightarrow>\<^isub>a M'"
   shows "M \<longrightarrow>\<^isub>a* M'"
 using a by blast
-
-lemma a_star_refl:
-  shows "M \<longrightarrow>\<^isub>a* M"
-  by blast
 
 lemma a_starE:
   assumes a: "M \<longrightarrow>\<^isub>a* M'"
   shows "M = M' \<or> (\<exists>N. M \<longrightarrow>\<^isub>a N \<and> N \<longrightarrow>\<^isub>a* M')"
 using a