/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | variable_munge.c | 40 int qux(int bbb) argument
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | tripleScript.sml | 92 \\ qpat_x_assum `!c. ~bbb` kall_tac 99 >- (qpat_x_assum `!x.bbb` (MP_TAC o Q.SPEC `x`) 117 \\ qpat_x_assum `!x.bbb` (MP_TAC o Q.SPEC `x`)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_ordinalScript.sml | 106 \\ Q.PAT_ASSUM `!x.bbb` MATCH_MP_TAC 110 \\ Q.PAT_ASSUM `!x.bbb` MATCH_MP_TAC 148 \\ Q.PAT_ASSUM `!x. bbb` MATCH_MP_TAC
|
H A D | milawa_execScript.sml | 467 \\ TRY (Q.PAT_X_ASSUM `!io.bbb` MP_TAC 468 \\ Q.PAT_X_ASSUM `!io.bbb` (STRIP_ASSUME_TAC o SPEC_ALL) 470 \\ Q.PAT_X_ASSUM `!io.bbb` (STRIP_ASSUME_TAC o Q.SPEC `STRCAT io io1`) 690 \\ Q.PAT_X_ASSUM `!b:string |-> SExp. bbb` MATCH_MP_TAC 1080 \\ Q.PAT_X_ASSUM `!x' x''. MEM (x',x'') ts ==> bbb` MP_TAC 1090 \\ Q.PAT_X_ASSUM `!sl:SExp list.bbb` ASSUME_TAC 1234 \\ Q.PAT_X_ASSUM `!x1 x2 x3 x4 x5. bbb ==> MR_ev (Or xx,yyy) zz` MATCH_MP_TAC 1300 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` MP_TAC) 1315 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` MP_TAC) 1389 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TA [all...] |
H A D | milawa_logicScript.sml | 596 \\ Q.PAT_X_ASSUM `!a.bbb` MATCH_MP_TAC \\ FULL_SIMP_TAC std_ss [] 604 \\ Q.PAT_X_ASSUM `!a.bbb` MATCH_MP_TAC \\ FULL_SIMP_TAC std_ss [] 924 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 932 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 969 \\ RES_TAC \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 970 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 975 \\ RES_TAC \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 976 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 1160 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC)) 1172 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz. bbb` ( [all...] |
H A D | milawa_proofpScript.sml | 386 (Q.PAT_X_ASSUM `!t.bbb ==> b2 ==> b3` (MP_TAC o Q.SPEC `e`) 389 (Q.PAT_X_ASSUM `!t.bbb ==> b2 ==> b3` (MP_TAC o Q.SPEC `e`) 392 (Q.PAT_X_ASSUM `!t.bbb ==> b2 ==> b3` (MP_TAC o Q.SPEC `l`) 493 \\ Q.PAT_X_ASSUM `!xs.bbb` (MP_TAC o Q.SPEC `[S''']`) 592 \\ Q.PAT_X_ASSUM `!ts.bbb` (fn th => (MP_TAC o Q.SPEC `l0`) th THEN 599 \\ STRIP_TAC \\ Q.PAT_X_ASSUM `!ts.bbb` (MP_TAC o Q.SPEC `l`) 849 (Q.PAT_X_ASSUM `!xx.bbb` (MATCH_MP_TAC o REWRITE_RULE [AND_IMP_INTRO]) 1482 \\ Q.PAT_X_ASSUM `!e. bbb ==> MilawaTrue ctxt e` MATCH_MP_TAC 1525 \\ Q.PAT_X_ASSUM `!xx.bbb` MATCH_MP_TAC 1699 \\ Q.PAT_X_ASSUM `!ts.bbb` (f [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | divideScript.sml | 65 THEN Q.PAT_X_ASSUM `!m.bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `m - (2 * n)`) 66 THEN Q.PAT_X_ASSUM `!m.bbb` (ASSUME_TAC o REWRITE_RULE [] o Q.SPECL [`m`,`2*n`]) 68 THEN Q.PAT_X_ASSUM `!m.bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o 146 THEN Q.PAT_X_ASSUM `!m l. bbb` 164 THEN Q.PAT_X_ASSUM `!m l. bbb` 187 THEN Q.PAT_X_ASSUM `!k.bbb` (STRIP_ASSUME_TAC o Q.SPEC `1`)
|
H A D | lisp_parseScript.sml | 150 \\ Q.PAT_X_ASSUM `!k. ?b. bbb` (STRIP_ASSUME_TAC o Q.SPEC `10 * k + (ORD h - 48)`) 165 \\ Q.PAT_X_ASSUM `!k. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`0`]) 320 \\ RES_TAC \\ Q.PAT_X_ASSUM `!t a b. bbb` (K ALL_TAC) 321 \\ REPEAT (Q.PAT_X_ASSUM `!r4. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`n2w (ORD h)`])) 380 \\ Q.PAT_X_ASSUM `!a. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 819 \\ Q.PAT_X_ASSUM `!s. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`STRCAT s (STRING h "")`,`P`]) 957 \\ Q.PAT_X_ASSUM `!r1 r2. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL 1025 \\ Q.PAT_X_ASSUM `!r1 r2. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL 1084 \\ Q.PAT_X_ASSUM `!xx. bb ==> bbb` (ASSUME_TAC o Q.SPEC `STRLEN t2`) 1097 \\ Q.PAT_X_ASSUM `!r1 r2. bbb` (STRIP_ASSUME_TA [all...] |
H A D | lisp_equalScript.sml | 183 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 197 \\ Q.PAT_X_ASSUM `!xxx. bbb` (ASSUME_TAC o RW1 [GSYM CONTAINER_def]) 220 \\ Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` 224 \\ Q.PAT_X_ASSUM `!x. bbb` 261 \\ Q.PAT_X_ASSUM `CONTAINER (!x. bbb)` 265 \\ Q.PAT_X_ASSUM `!x. bbb` 334 \\ ASM_REWRITE_TAC [] \\ Q.PAT_X_ASSUM `!x. bbb` (K ALL_TAC) 763 THEN1 (Q.PAT_X_ASSUM `!x. bbb ==> (f5 x = ft x)` MATCH_MP_TAC 768 \\ Q.PAT_X_ASSUM `!x. bbb ==> (f5 x = ft x)` MATCH_MP_TAC
|
H A D | lisp_proofScript.sml | 305 THEN Q.PAT_X_ASSUM `!x y stack l. ?x'. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`x`,`y`,` 317 THEN Q.PAT_X_ASSUM `!x y stack l. ?x'. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`x`,`y`,` 577 THEN Q.PAT_X_ASSUM `!x.bbb` (STRIP_ASSUME_TAC o Q.SPECL [`y`,`stack`,`l`]) 729 THEN Q.PAT_X_ASSUM `!a2.bbb` (ASSUME_TAC o 732 THEN Q.PAT_X_ASSUM `!x.bbb` (STRIP_ASSUME_TAC o Q.SPECL 854 THEN REPEAT STRIP_TAC THEN Q.PAT_X_ASSUM `!ys. bbb` MATCH_MP_TAC 890 THEN Q.PAT_X_ASSUM `!xs.bbb` MATCH_MP_TAC 901 THEN REPEAT STRIP_TAC THEN Q.PAT_X_ASSUM `!xs. bbb ==> bbbb` MATCH_MP_TAC
|
H A D | lisp_printScript.sml | 155 \\ Q.PAT_X_ASSUM `!p. bbb` MATCH_MP_TAC 271 \\ Q.PAT_X_ASSUM `!m. bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `n DIV 10`) 405 \\ Q.PAT_X_ASSUM `!a. bbb` (MP_TAC o Q.SPECL [`a2`,`(w + a) - a2`,`sym DELETE (a,h)`]) 526 \\ Q.PAT_X_ASSUM `~(bbb /\ cc)` MP_TAC 794 (Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` (K ALL_TAC) 827 (Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` (K ALL_TAC) 921 \\ Q.PAT_X_ASSUM `!m. bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `LSIZE (CAR (CDR t))`) 1044 \\ Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` (fn th => let val th = RW [CONTAINER_def] th in 1150 \\ Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC) 1257 \\ Q.PAT_X_ASSUM `bb = bbb * f [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_compilerScript.sml | 434 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!tttt.bbb` MATCH_MP_TAC 458 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!tttt.bbb` MATCH_MP_TAC 466 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 475 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 479 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 484 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 487 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 492 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 506 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 527 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TA [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_equalScript.sml | 198 \\ Q.PAT_X_ASSUM `!m.bbb` (MP_TAC o Q.SPEC `lisp_eq_measure ((w0n,x0n,w1n,x1n)::t) + (LENGTH t)`) 253 \\ IMP_RES_TAC lisp_inv_car \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 255 \\ IMP_RES_TAC lisp_inv_car \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 265 \\ IMP_RES_TAC lisp_inv_cdr \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 267 \\ IMP_RES_TAC lisp_inv_cdr \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 272 \\ Q.PAT_X_ASSUM `!m.bbb` (MP_TAC o Q.SPEC `lisp_eq_measure ((w04,CDR x0,w14,CDR x1)::(w00,CAR x0,w10,CAR x1)::ys) + LENGTH ((w00,CAR x0,w10,CAR x1)::ys)`) 309 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC))
|
H A D | lisp_bigopsScript.sml | 148 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 162 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 163 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 178 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`xs`,`IO_WRITE io (STRCAT (sexp2string_aux (S',T)) " . ")`,`F`]) 185 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`xs`,`IO_WRITE io (STRCAT (sexp2string_aux (S',T)) " . ")`,`F`]) 190 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`xs`,`IO_WRITE io (STRCAT (sexp2string_aux (S',T)) " ")`,`F`]) 196 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 197 \\ Q.PAT_X_ASSUM `!x1.bbb` MP_TAC 215 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TAC o Q.SPECL [`S0`,`Sym "T"::xs`,`IO_WRITE io (STRCAT "(" (STRCAT (sexp2string_aux (S',T)) " . "))`,`F`]) 226 (Q.PAT_X_ASSUM `!x1.bbb` (MP_TA [all...] |
H A D | lisp_invScript.sml | 329 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 473 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 552 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 591 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 704 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 785 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 845 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 900 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 948 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1151 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb [all...] |
H A D | lisp_correctnessScript.sml | 76 \\ Q.PAT_X_ASSUM `!p.bbb` (ASSUME_TAC o Q.SPECL [`p`,`STRCAT s (STRING h "")`]) 88 \\ Q.PAT_X_ASSUM `!s.bbb` MATCH_MP_TAC 270 (Q.PAT_X_ASSUM `!x0.bbb` MATCH_MP_TAC
|
H A D | lisp_compiler_opScript.sml | 736 (Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC) 737 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`x1`,`CDR x2`,`xs`,`SFIX (CAR x2)`,`[]`]) 1203 \\ Q.PAT_X_ASSUM `!code. bbb` (MP_TAC o Q.SPECL 3642 \\ REPEAT (Q.PAT_X_ASSUM `!x0.bbb` (STRIP_ASSUME_TAC o Q.SPEC `Val 0`)) 3659 \\ Q.PAT_X_ASSUM `!xs.bbb` MP_TAC 3660 \\ Q.PAT_X_ASSUM `!xs.bbb` (STRIP_ASSUME_TAC o Q.SPECL [`xsss`,`code`]) 3666 \\ Q.PAT_X_ASSUM `!xs.bbb` (STRIP_ASSUME_TAC o Q.SPECL [`xs'`,`WRITE_CODE code code1`]) 3682 \\ Q.PAT_X_ASSUM `!ys.bbb` (STRIP_ASSUME_TAC o RW [] o Q.SPECL [`xsss`,`code'`]) 3692 \\ Q.PAT_X_ASSUM `!x0:SExp.bbb` (STRIP_ASSUME_TAC o Q.SPEC `^COMPILE_CALL`) 3702 \\ REPEAT (Q.PAT_X_ASSUM `!x0:SExp.bbb` (STRIP_ASSUME_TA [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | progScript.sml | 68 \\ Q.PAT_X_ASSUM `!state r. bbb` (ASSUME_TAC o Q.SPECL [`state`,`r * r'`]) 90 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`state`,`r'`,`seq`]) 168 \\ Q.PAT_X_ASSUM `!x.bbb` MP_TAC 169 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`state`,`r`,`seq`]) 172 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`seq (i:num)`,`r`,`(\j. seq (i + j))`])
|
H A D | tailrecScript.sml | 78 \\ Q.PAT_X_ASSUM `!x. ?n. bbb` (STRIP_ASSUME_TAC o Q.SPEC `\n. FUNPOW step n x`)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/parse/ |
H A D | lisp_parseScript.sml | 34 \\ Q.PAT_X_ASSUM `!x. bbb ==> P x` MATCH_MP_TAC THEN1 355 \\ REPEAT (Q.PAT_X_ASSUM `bbb = t` (ASSUME_TAC o GSYM)) 503 \\ Cases_on `h = #"("` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 504 \\ Cases_on `h = #")"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 505 \\ Cases_on `h = #"'"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 506 \\ Cases_on `h = #"#"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 601 \\ Q.PAT_X_ASSUM `!ss ts. bbb` (ASSUME_TAC o Q.SPECL [`"'" ++ s_str3`,`[(Val 3,Val 1)] ++ t_str3`]) 627 \\ Q.PAT_X_ASSUM `!ss ts. bbb` (ASSUME_TAC o Q.SPECL [`s1 ++ s_str1 ++ s3 ++ s2`,`t1 ++ t_str1 ++ t3 ++ t2`]) 644 (Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (K ALL_TAC) 645 \\ Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (MATCH_MP_TA [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_codegenScript.sml | 311 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 315 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 319 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 323 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 327 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 331 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 335 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 339 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC
|
H A D | jit_incrementalScript.sml | 449 \\ Q.PAT_X_ASSUM `!i.bbb` (ASSUME_TAC o Q.SPECL [`i+1`,`n`,`j`]) 514 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 538 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 562 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 586 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 680 \\ Q.PAT_X_ASSUM `!i.bbb` MATCH_MP_TAC 725 \\ Q.PAT_X_ASSUM `!i.bbb` (ASSUME_TAC o Q.SPECL [`i+1`,`n`,`c`,`j`,`w`]) 786 \\ Q.PAT_X_ASSUM `!i.bbb` MATCH_MP_TAC 811 \\ Q.PAT_X_ASSUM `!r. bbb` (ASSUME_TAC o Q.SPEC `CODE_LOOP 0 j cs * 880 \\ Q.PAT_X_ASSUM `!cs n. bbb` (ASSUME_TA [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | arm_improved_gcScript.sml | 230 \\ Q.PAT_X_ASSUM `!ys.bbb` MATCH_MP_TAC \\ Q.EXISTS_TAC `zs` 246 \\ Q.PAT_X_ASSUM `!a.bb /\ bbbb ==> bbb` (ASSUME_TAC o Q.SPEC `a+1`) 250 \\ Q.PAT_X_ASSUM `bb ==> bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 435 \\ Q.PAT_X_ASSUM `!k. bbb ==> (m k = H_EMP)` MATCH_MP_TAC 532 \\ Q.PAT_X_ASSUM `!xx yy. bbb` (SEP_S_TAC ["arm_move_list","move_list","gc_inv"]) 585 \\ Q.PAT_X_ASSUM `!xx yy. bbb` (SEP_S_TAC ["arm_move_roots","move_list","gc_inv"]) 663 \\ Q.PAT_X_ASSUM `!m. m < e - i ==> bbb` ASSUME_TAC 704 \\ Q.PAT_X_ASSUM `!m. m < e - i ==> bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `e - i8`) 879 \\ Q.PAT_X_ASSUM `!k. bbb ==> (m4 k = H_EMP)` MATCH_MP_TAC
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/garbage-collector/ |
H A D | lisp_consScript.sml | 413 \\ Q.PAT_X_ASSUM `!p.bbb` (MP_TAC o Q.SPEC `p`) 421 \\ Q.PAT_X_ASSUM `!p.bbb` (MP_TAC o Q.SPEC `p`) 482 \\ Q.PAT_X_ASSUM `!ee ii. bbb` (MP_TAC o Q.SPECL [`e`,`i4`]) 488 \\ Q.PAT_X_ASSUM `bbb ==> ccc` MP_TAC \\ ASM_SIMP_TAC std_ss [] 553 \\ Q.PAT_X_ASSUM `!p. bbb ==> ccc` 561 \\ Q.PAT_X_ASSUM `!p. bbb ==> ccc`
|
H A D | stop_and_copyScript.sml | 614 \\ Q.PAT_X_ASSUM `bbb ==> full_heap (b + n + 1) e m2` MATCH_MP_TAC 656 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!k. bbb ==> (m k = H_EMP)` MATCH_MP_TAC 834 \\ Q.PAT_X_ASSUM `!k.bbb` MATCH_MP_TAC \\ DECIDE_TAC); 880 \\ Q.PAT_X_ASSUM `!z h f.bbb` (MP_TAC o Q.SPECL [ 1031 \\ Q.PAT_X_ASSUM `!a. bbb` (MP_TAC o Q.GEN `a` o Q.SPEC `(f3:num->num) a`) 1616 \\ Q.PAT_X_ASSUM `!a.bbb` (MP_TAC o Q.SPEC `k' + e`) 1635 (Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC) 1636 \\ Q.PAT_X_ASSUM `!x.bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 1645 (Q.PAT_X_ASSUM `!x.bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO])
|