adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

isabelle2022 lib: update Lib 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2022-11-01 16:06:54 +11:00 committed by Gerwin Klein
parent e101f37cfc
commit c6b137dfba
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/subgoal_focus/Subgoal_Methods.thy
View File

@ -171,7 +171,7 @@ let
let
val ((_,prem'),ctxt') = Variable.focus NONE prem ctxt;
val rule_prop = Thm.prop_of rule;
in Unify.matches_list (Context.Proof ctxt') [rule_prop] [prem'] end;
in is_none (Unify.matcher (Context.Proof ctxt') [rule_prop] [prem']) end;
in filter_prems_tac' ctxt (not o member matches rules) end;