/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient.sml | |
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
H A D | ind_rel.sml | 880 val imp = NOT_NOT th value 958 val imp = concl th1 value [all...] |
/seL4-l4v-10.1.1/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-10.1.1/HOL4/src/num/theories/ |
H A D | arithmeticScript.sml | 766 [let val imp = SPECL [���(m-n)*p���, value
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Term.sml | 1016 val imp = let value
|
H A D | Term.sig | 8 val imp : term value
|
/seL4-l4v-10.1.1/HOL4/src/bool/ |
H A D | boolScript.sml | 317 local val imp = ���$==>��� val notc = ���$~��� value 2241 and imp = ���$==>��� value
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | selftest.sml | 1067 val imp = ``!x:ind. P x /\ R x ==> ?y:'a. Q x y`` value
|
H A D | Prim_rec.sml | 713 val imp = GEN P (DISCH ex1P (SPECL [v1, v2] th2)) value
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Term.sml | 64 val imp = Const (imp_id,imp_ty) value
|
H A D | Term.sig | 10 val imp : term value
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_opsScript.sml | 293 val imp = lisp_inv_stack |> Q.SPECL [`p+3w::qs`,`tw2`] value 303 val imp = lisp_inv_stack |> Q.SPECL [`r2::qs`,`tw2`] value 313 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`tw2`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL value 324 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`tw2`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL value 334 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`HD qs`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL value 345 val imp = lisp_inv_stack |> Q.SPECL [`p+6w::qs`,`tw2`] value 373 val imp = generate_copy i j value 416 val imp = generate_copy i j value 417 val imp = DISCH_ALL (MATCH_MP (generate_car i) (UNDISCH imp)) value 461 val imp = generate_copy i j value 462 val imp = DISCH_ALL (MATCH_MP (generate_cdr i) (UNDISCH imp)) value 485 val imp = DISCH_ALL (MATCH_MP lisp_inv_type (UNDISCH (swap_thm i))) value 526 val imp = generate_sym i value 567 val imp = generate_val i value 594 val imp = UNDISCH lisp_inv_eq_zero value 595 val imp = DISCH_ALL (MATCH_MP (DISCH_ALL imp) (UNDISCH (swap_thm i))) value 634 val imp = UNDISCH (SIMP_RULE std_ss [] (SPEC (numSyntax.term_of_int n) lisp_inv_eq_val)) value 635 val imp = DISCH_ALL (MATCH_MP (DISCH_ALL imp) (UNDISCH (swap_thm i))) value 668 val imp = lemma value 700 val imp = RW1 [lemma] lisp_inv_less value 723 val imp = RW1 [lemma] lisp_inv_even value 759 val imp = lisp_inv_Val_n2w |> SPEC_ALL |> RW1 [GSYM AND_IMP_INTRO] value 781 val imp = generate_assign_val n_tm i value 814 val imp = generate_assign_sym n i value 833 val imp = generate_test_sym n i value 876 val imp = lisp_inv_error value 906 val imp = mc_is_quote_full_thm value 918 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_gc value 957 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4]) value 990 val imp = DISCH_ALL (LIST_CONJ [imp1,imp2,imp3,imp4]) value 1019 val imp = mc_full_equal_thm value 1078 val imp = lisp_inv_add value 1089 val imp = lisp_inv_add_nop value 1146 val imp = generate_add1 i value 1158 val imp = generate_add1_nop i value 1202 val imp = RW1 [lemma] lisp_inv_sub value 1223 val imp = generate_sub1 i value 1249 val imp = RW1 [lemma] lisp_inv_div2 value 1270 val imp = DISCH_ALL (el (i+1) (CONJUNCTS (UNDISCH mc_safe_car_thm))) value 1291 val imp = DISCH_ALL (el (i+1) (CONJUNCTS (UNDISCH mc_safe_cdr_thm))) value 1341 val imp = lisp_inv_swap0 value 1347 val imp = UNDISCH lisp_inv_nil value 1348 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 1349 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 1388 val imp = lisp_inv_swap0 value 1394 val imp = UNDISCH lisp_inv_zero value 1395 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 1396 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 1433 val imp = SIMP_RULE std_ss [LET_DEF] imp value 1484 val imp = Q.INST [`temp`|->`(31 -- 0) tw1`] lisp_inv_ignore_tw2 value 1501 val imp = lisp_inv_swap0 value 1536 val imp = Q.INST [`temp`|->`0w`] lisp_inv_ignore_tw2 value 1553 val imp = lisp_inv_swap0 value 1618 val imp = lisp_inv_swap0 value 1632 val imp = lisp_inv_swap0 value 1671 val imp = UNDISCH (CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM markerTheory.Abbrev_def])) lisp_inv_push) value 1678 val imp = (CONJ (UNDISCH_ALL thi) (UNDISCH_ALL thj)) value 1680 val imp = DISCH assum2 imp value 1733 val imp = generate_cons i j value 1736 val imp = DISCH assum imp value 1756 val imp = RW1 [lemma] lisp_inv_pop value 1783 val imp = generate_top i value 1818 val imp = RW1[lemma]lisp_inv_load value 1837 val imp = RW1[lemma]lisp_inv_store value 1866 val imp = RW1 [lemma] (SIMP_RULE std_ss [LET_DEF] lisp_inv_pops) value 1888 val imp = SIMP_RULE std_ss [LET_DEF] imp value 1905 val imp = mc_print_num_full_thm value 1920 val imp = mc_print_sym_full_thm value 1971 val imp = Q.INST [`temp`|->`5w`] lisp_inv_ignore_tw2 value 1990 val imp = Q.INST [`temp`|->`4w`] lisp_inv_ignore_tw2 value 2017 val imp = Q.INST [`temp`|->`11w`] lisp_inv_ignore_tw2 value 2168 val imp = SIMP_RULE std_ss [LET_DEF] mc_test_eof_thm value 2268 val imp = prove( value 2282 val imp = prove( value 2297 val imp = prove( value 2318 val imp = RW[GSYM AND_IMP_INTRO](RW1[CONJ_COMM]SPEC_COMPOSE) value 2329 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_set_thm value 2338 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_load_thm value 2347 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_store_thm value 2359 val imp = SIMP_RULE std_ss [LET_DEF] mc_load_amnt_thm value 2371 val imp = SIMP_RULE std_ss [LET_DEF] mc_pops_by_var_thm value 2383 val imp = mc_read_snd_code_thm value 2395 val imp = mc_const_load_thm value 2429 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4x]) value 2463 val imp = Q.INST [`temp`|->`12w`] lisp_inv_ignore_tw2 value 2479 val imp = lisp_inv_swap0 value 2502 val imp = mc_const_store_thm value 2535 val imp = mc_code_heap_space_thm value 2554 val imp = mc_code_heap_space_thm value 2579 val imp = SIMP_RULE std_ss [LET_DEF] imp value 2686 val imp = lisp_inv_load_test value 2696 val imp = lisp_inv_load_test_nop value 2725 val imp = lisp_inv_swap0 value 2735 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm value 2754 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4]) value 2808 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm value 2819 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm value 2882 val imp = lemma value 2908 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) value 2910 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2917 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil value 2919 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2947 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) value 2949 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2956 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil value 2958 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2988 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) value 2990 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 2997 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil value 2999 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) value 3021 val imp = lisp_inv_swap1 value 3030 val imp = mc_symbol_less_thm value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_parseScript.sml | 3125 val imp = arm_string2sexp_lemma value
|
H A D | lisp_opsScript.sml | 152 val imp = lisp_inv_cons value 164 val imp = lisp_inv_cons value 176 val imp = lisp_inv_cons value 191 val imp = lisp_inv_equal value 203 val imp = lisp_inv_equal value 215 val imp = lisp_inv_equal value 237 val imp = lisp_inv_test value 259 val imp = lisp_inv_test value 284 val imp = lisp_inv_test value 303 val imp = lisp_inv_test value 323 val imp = lisp_inv_test value 348 val imp = lisp_inv_test value 374 val imp = lisp_inv_move value 377 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 378 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 407 val imp = lisp_inv_move value 412 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 413 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 445 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 446 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 484 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 485 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 511 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 512 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 538 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) value 539 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) value 560 val imp = lisp_inv_move value 569 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) value 579 val imp = lisp_inv_move value 590 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) value 601 val imp = lisp_inv_move value 610 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) value 639 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),METIS_TAC [lisp_inv_car,lisp_inv_address]) value 663 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 687 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 717 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 743 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 769 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), value 791 val imp = lisp_inv_ADD value 792 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 804 val imp = lisp_inv_ADD value 805 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 817 val imp = lisp_inv_ADD value 818 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 833 val imp = lisp_inv_SUB value 834 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 846 val imp = lisp_inv_SUB value 847 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 859 val imp = lisp_inv_SUB value 860 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 873 val imp = lisp_inv_SUB1 value 874 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 875 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 876 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 877 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 878 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 892 val imp = lisp_inv_ADD1 value 893 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 894 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 895 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 896 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 897 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 916 val imp = lisp_inv_SUB1 value 917 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 918 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 919 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 920 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 921 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 939 val imp = lisp_inv_ADD1 value 940 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 941 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 942 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 943 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 944 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 964 val imp = lisp_inv_SUB1 value 965 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 966 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 967 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 968 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 969 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 984 val imp = lisp_inv_ADD1 value 985 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 986 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) value 987 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) value 988 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) value 989 val imp = RW1 [GSYM AND_IMP_INTRO] imp value 1008 val imp = lisp_inv_LESS value 1009 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1010 val imp = RW1 [EQ_SYM_EQ] imp value 1026 val imp = lisp_inv_LESS value 1027 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1028 val imp = RW1 [EQ_SYM_EQ] imp value 1047 val imp = lisp_inv_LESS value 1048 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1049 val imp = RW1 [EQ_SYM_EQ] imp value 1074 val imp = lisp_inv_MULT value 1075 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1087 val imp = lisp_inv_MULT value 1088 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1100 val imp = lisp_inv_MULT value 1101 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1113 val imp = lisp_inv_DIV value 1114 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1126 val imp = lisp_inv_DIV value 1127 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1139 val imp = lisp_inv_DIV value 1140 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1152 val imp = lisp_inv_MOD value 1153 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1165 val imp = lisp_inv_MOD value 1166 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1178 val imp = lisp_inv_MOD value 1179 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1206 val imp = lisp_inv_eq value 1207 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1233 val imp = lisp_inv_eq value 1234 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1258 val imp = lisp_inv_eq value 1259 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) value 1282 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) value 1283 val imp = RW1 [EQ_SYM_EQ] imp value 1308 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) value 1309 val imp = RW1 [EQ_SYM_EQ] imp value 1332 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) value 1333 val imp = RW1 [EQ_SYM_EQ] imp value 1383 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) value 1384 val imp = RW1 [EQ_SYM_EQ] imp value 1407 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) value 1408 val imp = RW1 [EQ_SYM_EQ] imp value 1429 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) value 1430 val imp = RW1 [EQ_SYM_EQ] imp value [all...] |
H A D | lisp_invScript.sml | 706 val imp = ((UNDISCH o SPEC_ALL o UNDISCH) lisp_inv_Val) value 711 val imp = (GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL) (MATCH_MP imp2 (MATCH_MP imp1 imp)) 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 | 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
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | prog_x64Lib.sml | 175 val imp = prove(goal, value 236 val imp = prove(goal, value 331 val imp = prove(goal, value
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/ |
H A D | prog_armLib.sml | 194 val imp = prove(goal, value 280 val imp = prove(goal, value 522 val imp = SPEC tm aligned_bx_lemma value
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 633 val imp = PURE_ONCE_REWRITE_CONV [rw] (mk_star(frame,p)) value 743 val imp = SEP_IMP_WEAKEN c x value 744 val imp = GEN v (CONV_RULE (BINOP_CONV (UNBETA_CONV v)) imp) value 756 val imp = SEP_IMP_WEAKEN (HIDE_INTRO tms) q value 767 val imp = SEP_IMP_WEAKEN (HIDE_INTRO tms) q value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | lisp_gcScript.sml | 1735 val imp = MATCH_MP LIMIT_LEMMA CARD_LESS_EQ_SUM_XSIZE value
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | reg_allocLib.sml | 503 val imp = auto_prove "initial_clean" (goal, value 509 val imp = initial_clean input_tm value
|