new version of "tryres" allowing multiple unifiers (apparently needed for
authorpaulson
Wed Nov 16 15:29:23 2005 +0100 (2005-11-16)
changeset 181757858b777569a
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
     1.1 --- a/src/HOL/Tools/meson.ML	Wed Nov 16 14:05:41 2005 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Nov 16 15:29:23 2005 +0100
     1.3 @@ -65,10 +65,13 @@
     1.4  
     1.5  (**** Operators for forward proof ****)
     1.6  
     1.7 +(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
     1.8 +fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
     1.9 +
    1.10  (*raises exception if no rules apply -- unlike RL*)
    1.11  fun tryres (th, rls) = 
    1.12    let fun tryall [] = raise THM("tryres", 0, th::rls)
    1.13 -        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
    1.14 +        | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
    1.15    in  tryall rls  end;
    1.16    
    1.17  (*Permits forward proof from rules that discharge assumptions*)