Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/NSA.ML
changeset 11655 923e4d0d36d5
parent 11383 297625089e80
child 11701 3d51fbf81c17 
--- a/src/HOL/Hyperreal/NSA.ML	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Hyperreal/NSA.ML	Wed Oct 03 20:54:16 2001 +0200
@@ -474,7 +474,7 @@
  ----------------------------------------------------------------------*)
 
 Goalw [Infinitesimal_def,approx_def] 
-        "x:Infinitesimal = (x @= #0)";
+        "(x:Infinitesimal) = (x @= #0)";
 by (Simp_tac 1);
 qed "mem_infmal_iff";
isabelle