Lines Matching defs:pre
96 val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH
97 val pre = RW [IF_IF,WORD_TIMES2] pre
107 in (th1,th3,pre) end;
113 val (th,def,pre) = basic_compile target tm
114 in (th,def,pre) :: compile_each tms end
120 val pre = RW [] (foldr (uncurry CONJ) TRUTH pres)
124 in (th,def,pre) end;
133 val pre = fetch "-" (name ^ "_pre_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
160 in (ys,def,pre) :: compile_each tms end
205 fun aux_fun_pre tm (def,pre) = let
207 in map (fn x => subst (fst (match_term def x)) pre) xs end
211 val pre = get_pre tm
212 in if pre = [] then f else FUN_COND (list_mk_conj pre, f) end
241 val (def,pre) = tailrec_define_with_pre tm pre_tm
242 val _ = (to_compile := (fname,(def,pre)) ::
244 in (def,pre) end;