equal
deleted
inserted
replaced
42 type ctxt = (string * typ) list * thm list |
42 type ctxt = (string * typ) list * thm list |
43 |
43 |
44 open Function_Common |
44 open Function_Common |
45 open Function_Lib |
45 open Function_Lib |
46 |
46 |
47 structure FunctionCongs = GenericDataFun |
47 structure FunctionCongs = Generic_Data |
48 ( |
48 ( |
49 type T = thm list |
49 type T = thm list |
50 val empty = [] |
50 val empty = [] |
51 val extend = I |
51 val extend = I |
52 fun merge _ = Thm.merge_thms |
52 val merge = Thm.merge_thms |
53 ); |
53 ); |
54 |
54 |
55 val get_function_congs = FunctionCongs.get o Context.Proof |
55 val get_function_congs = FunctionCongs.get o Context.Proof |
56 val map_function_congs = FunctionCongs.map |
56 val map_function_congs = FunctionCongs.map |
57 val add_function_cong = FunctionCongs.map o Thm.add_thm |
57 val add_function_cong = FunctionCongs.map o Thm.add_thm |