diff -r 41a2c9d5cd5d -r ea7a3cc64df5 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Jun 17 17:41:02 2023 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Jun 19 22:28:09 2023 +0200
@@ -10,6 +10,7 @@
   val smtlibC: SMT_Util.class
   val hosmtlibC: SMT_Util.class
   val bvsmlibC: SMT_Util.class
+  val realsmlibC: SMT_Util.class
   val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
@@ -25,6 +26,7 @@
 val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
 val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
 val bvsmlibC = smtlibC @ ["BV"] (* if BV are supported *)
+val realsmlibC = ["Real"]
 
 (* builtins *)
 
@@ -138,7 +140,7 @@
 
 val conjecture_prefix = "conjecture" (* FUDGE *)
 val hypothesis_prefix = "hypothesis" (* FUDGE *)
-val axiom_prefix = "axiom" (* FUDGE *)
+val axiom_prefix = "a" (* matching Alethe's convention *)
 
 fun assert_prefix_of_role SMT_Util.Conjecture = conjecture_prefix
   | assert_prefix_of_role SMT_Util.Hypothesis = hypothesis_prefix