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.
new version of "tryres" allowing multiple unifiers (apparently needed for
authorpaulson
Wed, 16 Nov 2005 15:29:23 +0100
changeset 18175 7858b777569a
parent 18174 c6e3c6516a23
child 18176 ae9bd644d106
new version of "tryres" allowing multiple unifiers (apparently needed for Skolemization of higher-order theorems)
src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/meson.ML	Wed Nov 16 14:05:41 2005 +0100
+++ b/src/HOL/Tools/meson.ML	Wed Nov 16 15:29:23 2005 +0100
@@ -65,10 +65,13 @@
 
 (**** Operators for forward proof ****)
 
+(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
+fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
+
 (*raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rls) = 
   let fun tryall [] = raise THM("tryres", 0, th::rls)
-        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
+        | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
   in  tryall rls  end;
   
 (*Permits forward proof from rules that discharge assumptions*)
isabelle