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.
Logic.implies;
authorwenzelm
Mon, 23 Jun 2008 23:45:46 +0200
changeset 27333 7095f775131a
parent 27332 94790a9620c3
child 27334 3f17273766f2
Logic.implies;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Mon Jun 23 23:45:45 2008 +0200
+++ b/src/Pure/drule.ML	Mon Jun 23 23:45:46 2008 +0200
@@ -146,7 +146,7 @@
 
 fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
 
-val implies = certify Term.implies;
+val implies = certify Logic.implies;
 fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
 
 (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
isabelle