Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added Least_Suc2
authoroheimb
Thu, 31 May 2001 16:50:13 +0200
changeset 11337 9d6d6a8966b9
parent 11336 fedccaeb5267
child 11338 779d289255f7
added Least_Suc2
src/HOL/Nat.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nat.ML	Thu May 31 16:50:04 2001 +0200
+++ b/src/HOL/Nat.ML	Thu May 31 16:50:13 2001 +0200
@@ -94,6 +94,11 @@
 by (blast_tac (claset() addIs [order_antisym]) 1); 
 qed "Least_Suc";
 
+Goal "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)";
+by (eatac (Least_Suc RS ssubst) 1 1);
+by (Asm_simp_tac 1);
+qed "Least_Suc2";
+
 
 (** min and max **)
isabelle