walther@59866: (* Title:  BaseDefinitions/thmC-def.sml
walther@59858:    Author: Walther Neuper
walther@59858:    (c) due to copyright terms
walther@59858: 
walther@59865: Probably this structure can be dropped due to improved reflection in Isabelle.
Walther@60650: Here is a minimum of code required for theory Know_Store,
walther@59919: further code see structure ThmC.
walther@59858: *)
walther@59865: signature THEOREM_ISAC_DEF =
walther@59858: sig
walther@59874:   type T
walther@59874:   eqtype id
walther@59861: 
Walther@60648:   val string_of_thm: Proof.context -> thm -> string
Walther@60648:   val string_of_thms: Proof.context -> thm list -> string
walther@59871: 
walther@59875: (* required in ProgLang BEFORE definition in ---------------vvv   *)
walther@59875:   val int_opt_of_string: string -> int option (* belongs to TermC *)
walther@59858: end
walther@59858: 
walther@59858: (**)
walther@59865: structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =
walther@59858: struct
walther@59858: (**)
walther@59858: 
walther@59887: type id = string; (* key into Know_Store, without point *)
walther@59874: type T = id * Thm.thm;
walther@59861: 
Walther@60648: fun string_of_thm ctxt thm =
Walther@60592:   let
Walther@60592:     val t = Thm.prop_of thm
Walther@60592:     val ctxt' = Config.put show_markup false ctxt
Walther@60592:   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
Walther@60648: fun string_of_thms ctxt thms = (strs2str o (map (string_of_thm ctxt))) thms
walther@59861: 
walther@59875: fun int_opt_of_string str = 
walther@59871:   let
walther@59871:     val ss = Symbol.explode str
walther@59871:     val ss' = case ss of "(" :: s => drop_last s | _ => ss
walther@59871:     val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss')
walther@59871:   in
walther@59871:     case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
walther@59871:   end;
walther@59871: 
walther@59858: (**)end(**)