blob: 4fde85eb3e328c6fb4757a944b8a27374618058c [file] [log] [blame] [edit]
--- BilbyFs_CorresProof.thy 2015-11-17 21:58:57.050814378 +1100
+++ BilbyFs_CorresProof.thy 2015-11-17 22:00:43.698453529 +1100
@@ -466,6 +466,12 @@
(* Additional Let rule for programs in K-normal form *)
lemmas corres_nested_let = corres_nested_let_base[OF LET_TRUE_def]
(* Run proofs for generated functions *)
+
+(* BilbyFs needs this for some reason *)
+end (* context BilbyFs *)
+declare [[unify_search_bound=999, unify_trace_bound=999]]
+context BilbyFs begin
+
(* ML{*
fun all_corres_goals corres_tac typing_tree_of time_limit ctxt (tab : obligations) =
let