| changeset 61594 | 07a903c8cc91 |
| parent 57492 | 74bf65a1910a |
| child 63167 | 0909deb8059b |
--- a/src/HOL/Nominal/Examples/Class1.thy Fri Nov 06 21:49:02 2015 +0100 +++ b/src/HOL/Nominal/Examples/Class1.thy Fri Nov 06 23:31:11 2015 +0100 @@ -5189,7 +5189,7 @@ using a2 a1 by (induct) (auto) -text {* congruence rules for \<longrightarrow>\<^sub>a* *} +text {* congruence rules for \<open>\<longrightarrow>\<^sub>a*\<close> *} lemma ax_do_not_a_star_reduce: shows "Ax x a \<longrightarrow>\<^sub>a* M \<Longrightarrow> M = Ax x a"