Searched defs:imp (Results 1 - 25 of 27) sorted by last modified time

12

/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient.sml
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dind_rel.sml880 val imp = NOT_NOT th value
958 val imp = concl th1 value
[all...]
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DUnicodeChars.sig113 val imp : string value
H A DUnicodeChars.sml44 val imp = U 0x21D2 value
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DarithmeticScript.sml766 [let val imp = SPECL [���(m-n)*p���, value
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/
H A DTerm.sml1016 val imp = let value
H A DTerm.sig8 val imp : term value
/seL4-l4v-10.1.1/HOL4/src/bool/
H A DboolScript.sml317 local val imp = ���$==>��� val notc = ���$~��� value
2241 and imp = ���$==>��� value
/seL4-l4v-10.1.1/HOL4/src/1/
H A Dselftest.sml1067 val imp = ``!x:ind. P x /\ R x ==> ?y:'a. Q x y`` value
H A DPrim_rec.sml713 val imp = GEN P (DISCH ex1P (SPECL [v1, v2] th2)) value
/seL4-l4v-10.1.1/HOL4/src/0/
H A DTerm.sml64 val imp = Const (imp_id,imp_ty) value
H A DTerm.sig10 val imp : term value
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_opsScript.sml293 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 Dlisp_parseScript.sml3125 val imp = arm_string2sexp_lemma value
H A Dlisp_opsScript.sml152 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 Dlisp_invScript.sml706 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 Dlisp_finalScript.sml210 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 DdivideScript.sml216 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 Djit_incrementalScript.sml2511 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 Dprog_x64Lib.sml175 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 Dprog_armLib.sml194 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 DhelperLib.sml633 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 Dlisp_gcScript.sml1735 val imp = MATCH_MP LIMIT_LEMMA CARD_LESS_EQ_SUM_XSIZE value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/
H A DdecompilerLib.sml1241 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 Dreg_allocLib.sml503 val imp = auto_prove "initial_clean" (goal, value
509 val imp = initial_clean input_tm value

Completed in 594 milliseconds

12