Lines Matching defs:def
113 val (th,def,pre) = basic_compile target tm
114 in (th,def,pre) :: compile_each tms end
119 val def = RW [] (foldr (uncurry CONJ) TRUTH defs)
124 in (th,def,pre) end;
132 val (th,def,_) = basic_compile target tm
134 val tm = concl def
135 in (target,th,def,pre):: compile_each tm ts end
138 fun prove_eq (target,th,def,pre) = let
140 val goal = mk_conj(mk_eq(f def,f last_def),mk_eq(f pre,f last_pre))
157 val (ys,def,pre) = compile_all_aux tm
158 val x2 = (car o fst o dest_eq o concl o SPEC_ALL) def
160 in (ys,def,pre) :: compile_each tms end
205 fun aux_fun_pre tm (def,pre) = let
206 val xs = find_terms (fn x => can (match_term def) x) tm
207 in map (fn x => subst (fst (match_term def x)) pre) xs end
241 val (def,pre) = tailrec_define_with_pre tm pre_tm
242 val _ = (to_compile := (fname,(def,pre)) ::
244 in (def,pre) end;
252 fun uses def =
253 (all_distinct o map (fst o dest_const) o filter (fn x => not (x = fconst def)) o
254 find_terms (fn x => mem x all_fconsts) o concl) def
255 val all_uses = map (fn (_,(def,_)) => ((fst o dest_const o fconst) def, uses def)) (!to_compile)