equal
deleted
inserted
replaced
107 end |
107 end |
108 |
108 |
109 exception CODE_CERT_GEN of string |
109 exception CODE_CERT_GEN of string |
110 |
110 |
111 fun simplify_code_eq ctxt def_thm = |
111 fun simplify_code_eq ctxt def_thm = |
112 Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm |
112 Local_Defs.unfold ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm |
113 |
113 |
114 (* |
114 (* |
115 quot_thm - quotient theorem (Quotient R Abs Rep T). |
115 quot_thm - quotient theorem (Quotient R Abs Rep T). |
116 returns: whether the Lifting package is capable to generate code for the abstract type |
116 returns: whether the Lifting package is capable to generate code for the abstract type |
117 represented by quot_thm |
117 represented by quot_thm |