isabelle-2021 arm: update SimplExportAndRefine
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
34873cdd4a
commit
0758ff13c1
|
@ -73,6 +73,10 @@ val dbg = ProveSimplToGraphGoals.new_debug
|
|||
};
|
||||
\<close>
|
||||
|
||||
context
|
||||
includes no_take_bit
|
||||
begin
|
||||
|
||||
(* If this fails, it can be debugged with the assistance of the
|
||||
script in TestGraphRefine.thy *)
|
||||
ML \<open>
|
||||
|
@ -95,3 +99,5 @@ val _ = ProveSimplToGraphGoals.print dbg "successes:" #successes;
|
|||
end
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue