/seL4-l4v-master/HOL4/src/experimental-kernel/ |
H A D | Term.sig | 8 val imp : term value
|
H A D | Term.sml | 1025 val imp = let value
|
/seL4-l4v-master/HOL4/src/0/ |
H A D | Term.sig | 10 val imp : term value
|
H A D | Term.sml | 61 val imp = Const (imp_id,imp_ty) value
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | divideScript.sml | 216 val imp = Q.SPECL [`r4`,`r3`] arm_div_thm value 240 val imp = Q.SPECL [`ecx`,`eax`] arm_div_thm value 276 val imp = Q.SPECL [`r4`,`r3`] arm_div_thm value
|
H A D | lisp_finalScript.sml | 210 val imp = arm_print_sexp_lemma value 211 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp value 212 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp) value 213 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp value 214 val imp = RW [] imp value 271 val imp = arm_print_sexp_lemma value 272 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp value 273 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp) value 274 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp value 275 val imp = RW [] imp value 421 val imp = arm_print_sexp_lemma value 422 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp value 423 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp) value 424 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp value 425 val imp = RW [] imp value [all...] |
H A D | lisp_invScript.sml | 710 val imp = ((UNDISCH o SPEC_ALL o UNDISCH) lisp_inv_Val) value 715 val imp = (GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL) (MATCH_MP imp2 (MATCH_MP imp1 imp)) value
|
H A D | lisp_opsScript.sml | 153 val imp = lisp_inv_cons value 165 val imp = lisp_inv_cons value 177 val imp = lisp_inv_cons value 192 val imp = lisp_inv_equal value 204 val imp = lisp_inv_equal value 216 val imp = lisp_inv_equal value 238 val imp = lisp_inv_test value 260 val imp = lisp_inv_test value 285 val imp = lisp_inv_test value 304 val imp = lisp_inv_test value 324 val imp = lisp_inv_test value 349 val imp = lisp_inv_test value 375 val imp = lisp_inv_move value 378 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 379 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 408 val imp = lisp_inv_move value 413 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 414 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 446 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 447 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 485 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 486 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 512 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 513 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 539 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 540 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 561 val imp = lisp_inv_move value 570 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) value 580 val imp = lisp_inv_move value 591 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) value 602 val imp = lisp_inv_move value 611 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) value 640 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),METIS_TAC [lisp_inv_car,lisp_inv_address]) value 664 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 688 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 718 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 744 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 770 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 792 val imp = lisp_inv_ADD value 793 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 805 val imp = lisp_inv_ADD value 806 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 818 val imp = lisp_inv_ADD value 819 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 834 val imp = lisp_inv_SUB value 835 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 847 val imp = lisp_inv_SUB value 848 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 860 val imp = lisp_inv_SUB value 861 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 874 val imp = lisp_inv_SUB1 value 875 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 876 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 877 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 878 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 879 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 893 val imp = lisp_inv_ADD1 value 894 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 895 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 896 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 897 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 898 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 917 val imp = lisp_inv_SUB1 value 918 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 919 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 920 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 921 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 922 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 940 val imp = lisp_inv_ADD1 value 941 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 942 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 943 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 944 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 945 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 965 val imp = lisp_inv_SUB1 value 966 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 967 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 968 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 969 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 970 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 985 val imp = lisp_inv_ADD1 value 986 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 987 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 988 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 989 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 990 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 1009 val imp = lisp_inv_LESS value 1010 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1011 val imp = RW1 [EQ_SYM_EQ] imp value 1027 val imp = lisp_inv_LESS value 1028 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1029 val imp = RW1 [EQ_SYM_EQ] imp value 1048 val imp = lisp_inv_LESS value 1049 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1050 val imp = RW1 [EQ_SYM_EQ] imp value 1075 val imp = lisp_inv_MULT value 1076 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1088 val imp = lisp_inv_MULT value 1089 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1101 val imp = lisp_inv_MULT value 1102 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1114 val imp = lisp_inv_DIV value 1115 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1127 val imp = lisp_inv_DIV value 1128 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1140 val imp = lisp_inv_DIV value 1141 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1153 val imp = lisp_inv_MOD value 1154 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1166 val imp = lisp_inv_MOD value 1167 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1179 val imp = lisp_inv_MOD value 1180 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1207 val imp = lisp_inv_eq value 1208 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1234 val imp = lisp_inv_eq value 1235 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1259 val imp = lisp_inv_eq value 1260 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1283 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) value 1284 val imp = RW1 [EQ_SYM_EQ] imp value 1309 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) value 1310 val imp = RW1 [EQ_SYM_EQ] imp value 1333 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) value 1334 val imp = RW1 [EQ_SYM_EQ] imp value 1384 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) value 1385 val imp = RW1 [EQ_SYM_EQ] imp value 1408 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) value 1409 val imp = RW1 [EQ_SYM_EQ] imp value 1430 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) value 1431 val imp = RW1 [EQ_SYM_EQ] imp value [all...] |
H A D | lisp_parseScript.sml | 3131 val imp = arm_string2sexp_lemma value
|
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sml | 283 val imp = allocate_registers n input_tm value
|
H A D | reg_allocLib.sml | 510 val imp = auto_prove "initial_clean" (goal, value 516 val imp = initial_clean input_tm value
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | prog_x64Lib.sml | 186 val imp = prove(goal, value 247 val imp = prove(goal, value 342 val imp = prove(goal, value
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | UnicodeChars.sig | 113 val imp : string value
|
H A D | UnicodeChars.sml | 44 val imp = U 0x21D2 value
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | lisp_gcScript.sml | 1736 val imp = MATCH_MP LIMIT_LEMMA CARD_LESS_EQ_SUM_XSIZE value
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/ |
H A D | prog_armLib.sml | 205 val imp = prove(goal, value 291 val imp = prove(goal, value 533 val imp = SPEC tm aligned_bx_lemma value
|
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_incrementalScript.sml | 2511 val imp = MATCH_INST xINC_SETUP_INTRO ``x86_inc_init (edx,esi,ebp,dh,h)`` value
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | selftest.sml | 1112 val imp = ``!x:ind. P x /\ R x ==> ?y:'a. Q x y`` value
|
H A D | Prim_rec.sml | 726 val imp = GEN P (DISCH ex1P (SPECL [v1, v2] th2)) value
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | ind_rel.sml | 870 val imp = NOT_NOT th value 948 val imp = concl th1 value [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_opsScript.sml | 296 val imp = lisp_inv_stack |> Q.SPECL [`p+3w::qs`,`tw2`] value 306 val imp = lisp_inv_stack |> Q.SPECL [`r2::qs`,`tw2`] value 316 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`tw2`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL value 327 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`tw2`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL value 337 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`HD qs`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL value 348 val imp = lisp_inv_stack |> Q.SPECL [`p+6w::qs`,`tw2`] value 376 val imp = generate_copy i j value 419 val imp = generate_copy i j value 420 val imp = DISCH_ALL (MATCH_MP (generate_car i) (UNDISCH imp)) value 464 val imp = generate_copy i j value 465 val imp = DISCH_ALL (MATCH_MP (generate_cdr i) (UNDISCH imp)) value 488 val imp = DISCH_ALL (MATCH_MP lisp_inv_type (UNDISCH (swap_thm i))) value 529 val imp = generate_sym i value 570 val imp = generate_val i value 597 val imp = UNDISCH lisp_inv_eq_zero value 598 val imp = DISCH_ALL (MATCH_MP (DISCH_ALL imp) (UNDISCH (swap_thm i))) value 637 val imp = UNDISCH (SIMP_RULE std_ss [] (SPEC (numSyntax.term_of_int n) lisp_inv_eq_val)) value 638 val imp = DISCH_ALL (MATCH_MP (DISCH_ALL imp) (UNDISCH (swap_thm i))) value 671 val imp = lemma value 703 val imp = RW1 [lemma] lisp_inv_less value 726 val imp = RW1 [lemma] lisp_inv_even value 762 val imp = lisp_inv_Val_n2w |> SPEC_ALL |> RW1 [GSYM AND_IMP_INTRO] value 784 val imp = generate_assign_val n_tm i value 817 val imp = generate_assign_sym n i value 836 val imp = generate_test_sym n i value 879 val imp = lisp_inv_error value 909 val imp = mc_is_quote_full_thm value 921 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_gc value 960 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4]) value 993 val imp = DISCH_ALL (LIST_CONJ [imp1,imp2,imp3,imp4]) value 1022 val imp = mc_full_equal_thm value 1081 val imp = lisp_inv_add value 1092 val imp = lisp_inv_add_nop value 1149 val imp = generate_add1 i value 1161 val imp = generate_add1_nop i value 1205 val imp = RW1 [lemma] lisp_inv_sub value 1226 val imp = generate_sub1 i value 1252 val imp = RW1 [lemma] lisp_inv_div2 value 1273 val imp = DISCH_ALL (el (i+1) (CONJUNCTS (UNDISCH mc_safe_car_thm))) value 1294 val imp = DISCH_ALL (el (i+1) (CONJUNCTS (UNDISCH mc_safe_cdr_thm))) value 1344 val imp = lisp_inv_swap0 value 1350 val imp = UNDISCH lisp_inv_nil value 1351 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 1352 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 1391 val imp = lisp_inv_swap0 value 1397 val imp = UNDISCH lisp_inv_zero value 1398 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 1399 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 1436 val imp = SIMP_RULE std_ss [LET_DEF] imp value 1487 val imp = Q.INST [`temp`|->`(31 -- 0) tw1`] lisp_inv_ignore_tw2 value 1504 val imp = lisp_inv_swap0 value 1539 val imp = Q.INST [`temp`|->`0w`] lisp_inv_ignore_tw2 value 1556 val imp = lisp_inv_swap0 value 1621 val imp = lisp_inv_swap0 value 1635 val imp = lisp_inv_swap0 value 1674 val imp = UNDISCH (CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM markerTheory.Abbrev_def])) lisp_inv_push) value 1681 val imp = (CONJ (UNDISCH_ALL thi) (UNDISCH_ALL thj)) value 1683 val imp = DISCH assum2 imp value 1736 val imp = generate_cons i j value 1739 val imp = DISCH assum imp value 1759 val imp = RW1 [lemma] lisp_inv_pop value 1786 val imp = generate_top i value 1821 val imp = RW1[lemma]lisp_inv_load value 1840 val imp = RW1[lemma]lisp_inv_store value 1869 val imp = RW1 [lemma] (SIMP_RULE std_ss [LET_DEF] lisp_inv_pops) value 1891 val imp = SIMP_RULE std_ss [LET_DEF] imp value 1908 val imp = mc_print_num_full_thm value 1923 val imp = mc_print_sym_full_thm value 1974 val imp = Q.INST [`temp`|->`5w`] lisp_inv_ignore_tw2 value 1993 val imp = Q.INST [`temp`|->`4w`] lisp_inv_ignore_tw2 value 2020 val imp = Q.INST [`temp`|->`11w`] lisp_inv_ignore_tw2 value 2171 val imp = SIMP_RULE std_ss [LET_DEF] mc_test_eof_thm value 2271 val imp = prove( value 2285 val imp = prove( value 2300 val imp = prove( value 2321 val imp = RW[GSYM AND_IMP_INTRO](RW1[CONJ_COMM]SPEC_COMPOSE) value 2332 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_set_thm value 2341 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_load_thm value 2350 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_store_thm value 2362 val imp = SIMP_RULE std_ss [LET_DEF] mc_load_amnt_thm value 2374 val imp = SIMP_RULE std_ss [LET_DEF] mc_pops_by_var_thm value 2386 val imp = mc_read_snd_code_thm value 2398 val imp = mc_const_load_thm value 2432 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4x]) value 2466 val imp = Q.INST [`temp`|->`12w`] lisp_inv_ignore_tw2 value 2482 val imp = lisp_inv_swap0 value 2505 val imp = mc_const_store_thm value 2538 val imp = mc_code_heap_space_thm value 2557 val imp = mc_code_heap_space_thm value 2582 val imp = SIMP_RULE std_ss [LET_DEF] imp value 2689 val imp = lisp_inv_load_test value 2699 val imp = lisp_inv_load_test_nop value 2728 val imp = lisp_inv_swap0 value 2738 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm value 2757 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4]) value 2811 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm value 2822 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm value 2885 val imp = lemma value 2911 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) value 2913 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2920 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil value 2922 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2950 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) value 2952 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2959 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil value 2961 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2991 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) value 2993 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 3000 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil value 3002 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 3024 val imp = lisp_inv_swap1 value 3033 val imp = mc_symbol_less_thm value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 654 val imp = PURE_ONCE_REWRITE_CONV [rw] (mk_star(frame,p)) value 764 val imp = SEP_IMP_WEAKEN c x value 765 val imp = GEN v (CONV_RULE (BINOP_CONV (UNBETA_CONV v)) imp) value 777 val imp = SEP_IMP_WEAKEN (HIDE_INTRO tms) q value 788 val imp = SEP_IMP_WEAKEN (HIDE_INTRO tms) q value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
H A D | decompilerLib.sml | 1241 val imp = SPEC (mk_abs(v,y)) (ISPEC c EXISTS_EQ_LEMMA) value
|
/seL4-l4v-master/HOL4/src/num/theories/ |
H A D | arithmeticScript.sml | 787 [let val imp = SPECL [���(m-n)*p���, value
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotient.sml | |