1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Thu Sep 23 13:47:16 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Fri Sep 24 14:18:10 2021 +0200
1.3 @@ -305,7 +305,7 @@
1.4 "~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
1.5 val simp_ctxt =
1.6 Proof_Context.init_global thy
1.7 - |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
1.8 + |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
1.9 val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
1.10
1.11 if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";