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/MacLaurin.ML
changeset 14269 502a7c95de73
parent 13187 e5434b822a96
child 14334 6137d24eef79 
--- a/src/HOL/Hyperreal/MacLaurin.ML	Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML	Fri Nov 28 12:09:37 2003 +0100
@@ -317,7 +317,7 @@
 by (induct_tac "n" 1);
 by (Simp_tac 1);
 by Auto_tac;
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1);
 by Auto_tac;
 by (cut_inst_tac [("f","diff 0"),
                  ("diff","diff"),
isabelle