equal
deleted
inserted
replaced
143 apply (simp add: Node_def Push_def) |
143 apply (simp add: Node_def Push_def) |
144 apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) |
144 apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) |
145 done |
145 done |
146 |
146 |
147 |
147 |
148 subsubsection{*Freeness: Distinctness of Constructors*} |
148 subsection{*Freeness: Distinctness of Constructors*} |
149 |
149 |
150 (** Scons vs Atom **) |
150 (** Scons vs Atom **) |
151 |
151 |
152 lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)" |
152 lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)" |
153 apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) |
153 apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) |