Lines Matching refs:bb
148 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `bb ==> cc` (K ALL_TAC))
545 Q.PAT_X_ASSUM `!x y. bb` MATCH_MP_TAC \\ Q.EXISTS_TAC `g`
617 \\ Q.PAT_X_ASSUM `!s a f g. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
636 \\ Q.PAT_X_ASSUM `!s a f g. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
1008 \\ Q.PAT_X_ASSUM `!m. bb ==> ccc` (ASSUME_TAC o
1083 \\ Q.PAT_X_ASSUM `!xx. bb ==> bbb` (ASSUME_TAC o Q.SPEC `STRLEN t2`)
1085 \\ Q.PAT_X_ASSUM `!xx. bb` (ASSUME_TAC o RW [] o Q.SPEC `t2`)
1264 \\ Q.PAT_X_ASSUM `~bb` (K ALL_TAC)
1781 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
1814 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
1870 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
1926 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
1953 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
1997 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
2035 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
2075 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
2107 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)