| --- 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 |