(* Title:  BaseDefinitions/thmC-def.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Probably this structure can be dropped due to improved reflection in Isabelle.

 Here is a minimum of code required for theory Know_Store,

 further code see structure ThmC.

 *)

 signature THEOREM_ISAC_DEF =

 sig

   type T

   eqtype id

   val string_of_thm: thm -> string

   val string_of_thms: thm list -> string

 (* required in ProgLang BEFORE definition in ---------------vvv   *)

   val int_opt_of_string: string -> int option (* belongs to TermC *)

 end

 (**)

 structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =

 struct

 (**)

 type id = string; (* key into Know_Store, without point *)

 type T = id * Thm.thm;

 (*this is from times before the introduction of sessions*)

 fun string_of_thm thm =

   let

     val t = Thm.prop_of thm

     val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))

     val ctxt' = Config.put show_markup false ctxt

   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

 fun string_of_thms thms = (strs2str o (map string_of_thm)) thms

 fun int_opt_of_string str = 

   let

     val ss = Symbol.explode str

     val ss' = case ss of "(" :: s => drop_last s | _ => ss

     val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss')

   in

     case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE

   end;

 (**)end(**)