src/HOL/Univ.ML
changeset 8114 09a7a180cc99
parent 7255 853bdbe9973d
child 8292 93e125b21220
equal deleted inserted replaced
8113:7110358acded 8114:09a7a180cc99
   204 
   204 
   205 Addsimps [apfst_conv];
   205 Addsimps [apfst_conv];
   206 AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
   206 AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
   207 
   207 
   208 
   208 
   209 Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0";
   209 Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
   210 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
   210 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
   211 by (rtac Least_equality 1);
   211 by (rtac Least_equality 1);
   212 by (rtac refl 1);
   212 by (rtac refl 1);
   213 by (etac less_zeroE 1);
   213 by (etac less_zeroE 1);
   214 qed "ndepth_K0";
   214 qed "ndepth_K0";