| changeset 10832 | e33b47e4246d |
| parent 10711 | a9f6994fb906 |
| child 10850 | e1a793957a8f |
--- a/src/HOL/NatDef.ML Tue Jan 09 15:18:07 2001 +0100 +++ b/src/HOL/NatDef.ML Tue Jan 09 15:22:13 2001 +0100 @@ -4,7 +4,7 @@ Copyright 1991 University of Cambridge *) -Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))"; +Goal "mono(%X. {Zero_Rep} Un Suc_Rep`X)"; by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1)); qed "Nat_fun_mono";