Lines Matching defs:def
342 fun guess_length_of_code def = let
343 val tm = def |> SIMP_RULE std_ss [word_arith_lemma1] |> SPEC_ALL |> concl |> cdr
355 fun derive_cs_assign def cs_thm = let
356 val n = numSyntax.term_of_int (guess_length_of_code def)
363 val new_code = (def |> Q.SPECL [`cs`,`p+6w`] |> concl |> dest_eq |> fst)
365 (def |> Q.SPECL [`p+6w`] |> concl |> dest_eq |> fst)
376 val def = abbrev_code_for_compile_inst_def
378 in derive_cs_assign def cs_thm end;
381 val def = abbrev_code_for_compile_def
383 in derive_cs_assign def cs_thm end;
386 val def = abbrev_code_for_print_def
388 in derive_cs_assign def cs_thm end;
391 val def = abbrev_code_for_equal_def
393 in derive_cs_assign def cs_thm end;
396 val def = abbrev_code_for_cons_def
398 in derive_cs_assign def cs_thm end;
401 val def = abbrev_code_for_parse_def
403 in derive_cs_assign def cs_thm end;