Searched defs:imp (Results 1 - 25 of 27) sorted by relevance

12

/seL4-l4v-master/HOL4/src/experimental-kernel/
H A DTerm.sig8 val imp : term value
H A DTerm.sml1025 val imp = let value
/seL4-l4v-master/HOL4/src/0/
H A DTerm.sig10 val imp : term value
H A DTerm.sml61 val imp = Const (imp_id,imp_ty) value
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
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
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 Dlisp_invScript.sml710 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 Dlisp_opsScript.sml153 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 Dlisp_parseScript.sml3131 val imp = arm_string2sexp_lemma value
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sml283 val imp = allocate_registers n input_tm value
H A Dreg_allocLib.sml510 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 Dprog_x64Lib.sml186 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 DUnicodeChars.sig113 val imp : string value
H A DUnicodeChars.sml44 val imp = U 0x21D2 value
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/
H A Dlisp_gcScript.sml1736 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 Dprog_armLib.sml205 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 Djit_incrementalScript.sml2511 val imp = MATCH_INST xINC_SETUP_INTRO ``x86_inc_init (edx,esi,ebp,dh,h)`` value
/seL4-l4v-master/HOL4/src/1/
H A Dselftest.sml1112 val imp = ``!x:ind. P x /\ R x ==> ?y:'a. Q x y`` value
H A DPrim_rec.sml726 val imp = GEN P (DISCH ex1P (SPECL [v1, v2] th2)) value
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dind_rel.sml870 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 Dlisp_opsScript.sml296 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 DhelperLib.sml654 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 DdecompilerLib.sml1241 val imp = SPEC (mk_abs(v,y)) (ISPEC c EXISTS_EQ_LEMMA) value
/seL4-l4v-master/HOL4/src/num/theories/
H A DarithmeticScript.sml787 [let val imp = SPECL [���(m-n)*p���, value
/seL4-l4v-master/HOL4/src/quotient/src/
H A Dquotient.sml

Completed in 388 milliseconds

12