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/Decision_Procs/cooper_tac.ML
changeset 35625 9c818cab0dd0
parent 33004 715566791eb0
child 36692 54b64d4ad524 
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -66,7 +66,7 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
+fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
     val thy = ProofContext.theory_of ctxt
isabelle