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

Isabelle2018 lib: Apply_Trace

This commit is contained in:
Gerwin Klein 2018-06-09 16:40:50 +10:00
parent 349e8a0411
commit 84081d1206
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/Apply_Trace.thy
View File

@ -290,7 +290,7 @@ let
val deps = case query of SOME (raw_query,pos) =>
let
val pos' = perhaps (try (Position.advance_offset 1)) pos;
val pos' = perhaps (try (Position.advance_offsets 1)) pos;
val q = Find_Theorems.read_query pos' raw_query;
val results = Find_Theorems.find_theorems_cmd ctxt (SOME thm) (SOME 1000000000) false q
|> snd