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/HOLCF/domain/theorems.ML
changeset 18057 ad97e231bf8a
parent 17985 d5d576b72371
child 18083 cf7669049df5 
--- a/src/HOLCF/domain/theorems.ML	Wed Nov 02 14:46:49 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML	Wed Nov 02 14:46:51 2005 +0100
@@ -45,7 +45,7 @@
                                 cut_facts_tac prems 1,
                                 fast_tac HOL_cs 1]);
 
-val dist_eqI = prove_goal Porder.thy "!!x::'a::po. ~ x << y ==> x ~= y" 
+val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
              (fn prems => [
                (blast_tac (claset() addDs [antisym_less_inverse]) 1)]);
 (*
isabelle