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.
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
authorwenzelm
Thu, 24 Feb 2000 15:59:44 +0100
changeset 8292 93e125b21220
parent 8291 5469b894f30b
child 8293 4a0e17cf8f70
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
src/HOL/Univ.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Univ.ML	Thu Feb 24 15:58:10 2000 +0100
+++ b/src/HOL/Univ.ML	Thu Feb 24 15:59:44 2000 +0100
@@ -425,7 +425,7 @@
 
 val [p1, p2] = Goalw [o_def]
      "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
-by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
+by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
 by (rtac ext 1);
 by (rtac (p1 RS FunsD RS rangeE) 1);
 by (etac (exI RS (select_eq_Ex RS iffD2)) 1);
isabelle