1 (* Title: BaseDefinitions/thmC-def.sml
3 (c) due to copyright terms
5 Probably this structure can be dropped due to improved reflection in Isabelle.
6 Here is a minimum of code required for theory Know_Store,
7 further code see structure ThmC.
9 signature THEOREM_ISAC_DEF =
14 val string_of_thm: Proof.context -> thm -> string
15 val string_of_thms: Proof.context -> thm list -> string
17 (* required in ProgLang BEFORE definition in ---------------vvv *)
18 val int_opt_of_string: string -> int option (* belongs to TermC *)
22 structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =
26 type id = string; (* key into Know_Store, without point *)
27 type T = id * Thm.thm;
29 fun string_of_thm ctxt thm =
31 val t = Thm.prop_of thm
32 val ctxt' = Config.put show_markup false ctxt
33 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
34 fun string_of_thms ctxt thms = (strs2str o (map (string_of_thm ctxt))) thms
36 fun int_opt_of_string str =
38 val ss = Symbol.explode str
39 val ss' = case ss of "(" :: s => drop_last s | _ => ss
40 val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss')
42 case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE