Lines Matching defs:def
91 fun convert1 (env,def) =
92 let val def1 = Normal.pre_process def
100 fun convert1a (env,def) =
101 let val def1 = convert1 def
108 fun convert1b (env,def) =
109 let val def1 = convert1a (env,def)
120 fun convert2 (env,def) =
121 let val def1 = convert1 (env,def)
129 fun convert2a (env,def) =
130 let val def1 = convert1a (env,def)
140 fun convert3 (env,def) =
141 let val def1 = convert2 (env,def)
215 fun redefine def =
217 val (fname, fbody) = dest_eq (concl def)
219 val def1 = CONV_RULE (RHS_CONV pairLib.GEN_BETA_CONV) (AP_THM def args)
232 val (def', ind') =
249 (def',ind')
259 fun f_compile_one def = hd (resultOf (f_compile_basic [def] false));
268 fun b_compile_one (def, ind) =
270 val (th,strs) = arm_compilerLib.arm_compile (SPEC_ALL def) ind (!style)
271 val code = fetch "-" (#1 (dest_const (#1 (head def))) ^ "_code1_def")