1(* Title: Pure/thm_name.ML 2 Author: Makarius 3 4Systematic naming of individual theorems, as selections from multi-facts. 5 6 (NAME, 0): the single entry of a singleton fact NAME 7 (NAME, i): entry i of a non-singleton fact (1 <= i <= length) 8*) 9 10signature THM_NAME = 11sig 12 type T = string * int 13 val ord: T ord 14 val print: T -> string 15 val flatten: T -> string 16 val make_list: string -> thm list -> (T * thm) list 17end; 18 19structure Thm_Name: THM_NAME = 20struct 21 22type T = string * int; 23val ord = prod_ord string_ord int_ord; 24 25fun print (name, index) = 26 if name = "" orelse index = 0 then name 27 else name ^ enclose "(" ")" (string_of_int index); 28 29fun flatten (name, index) = 30 if name = "" orelse index = 0 then name 31 else name ^ "_" ^ string_of_int index; 32 33fun make_list name [thm: thm] = [((name, 0), thm)] 34 | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms; 35 36end; 37