equal
deleted
inserted
replaced
254 |
254 |
255 Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq]; |
255 Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq]; |
256 |
256 |
257 |
257 |
258 goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0"; |
258 goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0"; |
259 by (sstac [Node_K0_I RS Abs_Node_inverse, split] 1); |
259 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]); |
260 by (rtac Least_equality 1); |
260 by (rtac Least_equality 1); |
261 by (rtac refl 1); |
261 by (rtac refl 1); |
262 by (etac less_zeroE 1); |
262 by (etac less_zeroE 1); |
263 qed "ndepth_K0"; |
263 qed "ndepth_K0"; |
264 |
264 |