moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
(* Author: Christian Urban+ −
+ −
data about nominal datatypes + −
*)+ −
+ −
signature NOMINAL_DT_DATA =+ −
sig+ −
type info =+ −
{inject : thm list,+ −
distinct : thm list,+ −
strong_inducts : thm list,+ −
strong_exhaust : thm list}+ −
+ −
val get_all_info: Proof.context -> (string * info) list+ −
val get_info: Proof.context -> string -> info option+ −
val the_info: Proof.context -> string -> info + −
val register_info: (string * info) -> Context.generic -> Context.generic+ −
val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list+ −
end+ −
+ −
structure Nominal_Dt_Data: NOMINAL_DT_DATA =+ −
struct+ −
+ −
(* information generated by nominal_datatype *)+ −
type info =+ −
{inject : thm list,+ −
distinct : thm list,+ −
strong_inducts : thm list,+ −
strong_exhaust : thm list}+ −
+ −
structure NominalData = Generic_Data+ −
(type T = info Symtab.table+ −
val empty = Symtab.empty+ −
val extend = I+ −
val merge = Symtab.merge (K true))+ −
+ −
val get_all_info = Symtab.dest o NominalData.get o Context.Proof+ −
val get_info = Symtab.lookup o NominalData.get o Context.Proof+ −
val register_info = NominalData.map o Symtab.update+ −
+ −
fun the_info thy name =+ −
(case get_info thy name of+ −
SOME info => info+ −
| NONE => error ("Unknown nominal datatype " ^ quote name))+ −
+ −
fun mk_infos ty_names inject distinct strong_inducts strong_exhaust =+ −
let+ −
fun aux ty_name =+ −
(ty_name, {inject = inject,+ −
distinct = distinct,+ −
strong_inducts = strong_inducts,+ −
strong_exhaust = strong_exhaust + −
})+ −
in+ −
map aux ty_names+ −
end+ −
+ −
+ −
end+ −