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.
Simplifid proofs.
authornipkow
Sun, 27 Oct 1996 13:47:02 +0100
changeset 2130 53b6e0bc8ccf
parent 2129 2ffe6e24f38d
child 2131 3106a99d30a5
Simplifid proofs.
src/HOL/IOA/NTP/Lemmas.ML file | annotate | diff | comparison | revisions
src/HOL/Lex/Prefix.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/IOA/NTP/Lemmas.ML	Fri Oct 25 15:02:09 1996 +0200
+++ b/src/HOL/IOA/NTP/Lemmas.ML	Sun Oct 27 13:47:02 1996 +0100
@@ -75,7 +75,6 @@
   by (nat_ind_tac "x" 1);
   by (Simp_tac 1);
   by (Asm_simp_tac 1);
-  by (Fast_tac 1);
 qed "nonzero_is_succ";
 
 goal Arith.thy "(m::nat) < n --> m + p < n + p";
--- a/src/HOL/Lex/Prefix.ML	Fri Oct 25 15:02:09 1996 +0200
+++ b/src/HOL/Lex/Prefix.ML	Sun Oct 27 13:47:02 1996 +0100
@@ -21,7 +21,6 @@
 goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (Fast_tac 1);
 by (Simp_tac 1);
 qed "prefix_Nil";
 Addsimps [prefix_Nil];
@@ -31,7 +30,6 @@
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (Fast_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "prefix_Cons";
isabelle