| changeset 8114 | 09a7a180cc99 |
| parent 7255 | 853bdbe9973d |
| child 8292 | 93e125b21220 |
--- a/src/HOL/Univ.ML Fri Jan 07 11:04:15 2000 +0100 +++ b/src/HOL/Univ.ML Fri Jan 07 11:06:03 2000 +0100 @@ -206,7 +206,7 @@ AddIffs [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq]; -Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0"; +Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0"; by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]); by (rtac Least_equality 1); by (rtac refl 1);