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.thy
changeset 27239 f2f42f9fa09d
parent 27227 184d7601c062 
--- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Jun 16 22:13:39 2008 +0200
@@ -50,7 +50,7 @@
 
 fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
   resolve_tac @{thms deriv_rulesI} i ORELSE
-    ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)]
+    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
                      @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
 
 fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
isabelle