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.
tidied
authorpaulson
Thu, 12 Oct 2000 12:26:30 +0200
changeset 10201 b52140d1a7bc
parent 10200 abdab72b8c7a
child 10202 9e8b4bebc940
tidied
src/HOL/Real/Hyperreal/HyperNat.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Real/Hyperreal/HyperNat.ML	Thu Oct 12 12:19:15 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperNat.ML	Thu Oct 12 12:26:30 2000 +0200
@@ -134,7 +134,7 @@
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_add_congruent2";
 
@@ -188,7 +188,7 @@
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_minus_congruent2";
  
@@ -279,7 +279,7 @@
  -----------------------------------------------------------*)
 Goalw [congruent2_def]
     "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "hypnat_mult_congruent2";
isabelle