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.
Removed Fast_tac made redundant by addition of de Morgan laws
authorpaulson
Thu, 10 Oct 1996 10:45:20 +0200
changeset 2081 c2da3ca231ab
parent 2080 12eed4cec935
child 2082 8659e3063a30
Removed Fast_tac made redundant by addition of de Morgan laws
src/HOL/Nat.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nat.ML	Wed Oct 09 13:50:28 1996 +0200
+++ b/src/HOL/Nat.ML	Thu Oct 10 10:45:20 1996 +0200
@@ -450,7 +450,6 @@
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (Fast_tac 1);
 qed "Suc_leD";
 
 (* stronger version of Suc_leD *)
isabelle