7293

1 
(* Title: HOL/Datatype.ML


2 
ID: $Id$

11954

3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

7293

5 
*)


6 

11954

7 
(** legacy ML bindings **)


8 


9 
structure bool =


10 
struct


11 
val distinct = thms "bool.distinct";


12 
val inject = thms "bool.inject";


13 
val exhaust = thm "bool.exhaust";


14 
val cases = thms "bool.cases";


15 
val split = thm "bool.split";


16 
val split_asm = thm "bool.split_asm";


17 
val induct = thm "bool.induct";


18 
val recs = thms "bool.recs";


19 
val simps = thms "bool.simps";


20 
val size = thms "bool.size";


21 
end;


22 


23 
structure sum =


24 
struct


25 
val distinct = thms "sum.distinct";


26 
val inject = thms "sum.inject";


27 
val exhaust = thm "sum.exhaust";


28 
val cases = thms "sum.cases";


29 
val split = thm "sum.split";


30 
val split_asm = thm "sum.split_asm";


31 
val induct = thm "sum.induct";


32 
val recs = thms "sum.recs";


33 
val simps = thms "sum.simps";


34 
val size = thms "sum.size";


35 
end;


36 


37 
structure unit =


38 
struct


39 
val distinct = thms "unit.distinct";


40 
val inject = thms "unit.inject";


41 
val exhaust = thm "unit.exhaust";


42 
val cases = thms "unit.cases";


43 
val split = thm "unit.split";


44 
val split_asm = thm "unit.split_asm";


45 
val induct = thm "unit.induct";


46 
val recs = thms "unit.recs";


47 
val simps = thms "unit.simps";


48 
val size = thms "unit.size";


49 
end;


50 


51 
structure prod =


52 
struct


53 
val distinct = thms "prod.distinct";


54 
val inject = thms "prod.inject";


55 
val exhaust = thm "prod.exhaust";


56 
val cases = thms "prod.cases";


57 
val split = thm "prod.split";


58 
val split_asm = thm "prod.split_asm";


59 
val induct = thm "prod.induct";


60 
val recs = thms "prod.recs";


61 
val simps = thms "prod.simps";


62 
val size = thms "prod.size";


63 
end;


64 

12918

65 
structure option =


66 
struct


67 
val distinct = thms "option.distinct";


68 
val inject = thms "option.inject";


69 
val exhaust = thm "option.exhaust";


70 
val cases = thms "option.cases";


71 
val split = thm "option.split";


72 
val split_asm = thm "option.split_asm";


73 
val induct = thm "option.induct";


74 
val recs = thms "option.recs";


75 
val simps = thms "option.simps";


76 
val size = thms "option.size";


77 
end;

7293

78 

12918

79 
val elem_o2s = thm "elem_o2s";


80 
val not_None_eq = thm "not_None_eq";


81 
val not_Some_eq = thm "not_Some_eq";


82 
val o2s_empty_eq = thm "o2s_empty_eq";


83 
val option_caseE = thm "option_caseE";


84 
val option_map_None = thm "option_map_None";


85 
val option_map_Some = thm "option_map_Some";


86 
val option_map_def = thm "option_map_def";


87 
val option_map_eq_Some = thm "option_map_eq_Some";


88 
val option_map_o_sum_case = thm "option_map_o_sum_case";


89 
val ospec = thm "ospec";


90 
val sum_case_inject = thm "sum_case_inject";


91 
val sum_case_weak_cong = thm "sum_case_weak_cong";


92 
val surjective_sum = thm "surjective_sum";
