src/HOL/HOL.thy

 val evaluation_meth =
   Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1));
 
 in
 
+val evaluation_conv = evaluation_conv;
+
 val eq_codegen_setup = Codegen.add_codegen "eq_codegen" eq_codegen;
 
 val evaluation_oracle_setup =
   Theory.add_oracle ("Evaluation", evaluation_oracle) #>
   Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation");

 
 val normalization_meth =
   Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI,refl] 1));
 
 in
+
+val normalization_conv = normalization_conv;
 
 val normalization_oracle_setup =
   Theory.add_oracle ("Normalization", normalization_oracle) #>
   Method.add_method ("normalization", normalization_meth, "solve goal by normalization");