/seL4-l4v-master/HOL4/tools/Holmake/tests/holdep/errors/ |
H A D | comment_unterm.sml | 1 val foo = 3 (* comment here
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | check_sources.scala | 19 Output.warning("Illegal file-name on Windows" + Position.here(file_pos)) 31 Position.here(line_pos(i))) 34 catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) } 37 Output.warning("TAB character" + Position.here(line_pos(i))) 41 Output.warning("CR character" + Position.here(file_pos)) 44 Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | check_sources.scala | 19 Output.warning("Illegal file-name on Windows" + Position.here(file_pos)) 31 Position.here(line_pos(i))) 34 catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) } 37 Output.warning("TAB character" + Position.here(line_pos(i))) 41 Output.warning("CR character" + Position.here(file_pos)) 44 Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
|
/seL4-l4v-master/HOL4/examples/CCS/ |
H A D | CoarsestCongrScript.sml | 54 >> rpt STRIP_TAC (* 2 sub-goals here *) 56 Cases_on `u` >| (* 2 sub-goals here *) 71 Cases_on `u` >| (* 2 sub-goals here *) 91 rpt STRIP_TAC (* 3 sub-goals here *) 110 >> Cases_on `?E. TRANS p tau E /\ WEAK_EQUIV E q` (* 2 sub-goals here *) 113 REWRITE_TAC [OBS_CONGR] >> rpt STRIP_TAC >| (* 2 sub-goals here *) 115 Cases_on `u` \\ (* 2 sub-goals here, sharing initial tacticals *) 132 Cases_on `?E. TRANS q tau E /\ WEAK_EQUIV p E` >| (* 2 sub-goals here *) 135 REWRITE_TAC [OBS_CONGR] >> rpt STRIP_TAC >| (* 2 sub-goals here *) 143 Cases_on `u` \\ (* 2 sub-goals here, sharin [all...] |
H A D | StrongLawsScript.sml | 28 >> CONJ_TAC (* 2 sub-goals here *) 37 rpt STRIP_TAC >| (* 4 sub-goals here *) 63 >> CONJ_TAC (* 2 sub-goals here *) 72 rpt STRIP_TAC >| (* 4 sub-goals here *) 97 >> CONJ_TAC (* 2 sub-goals here *) 107 rpt STRIP_TAC >| (* 4 sub-goals here *) 141 >> CONJ_TAC (* 2 sub-goals here *) 234 >> CONJ_TAC (* 2 sub-goals here *) 242 rpt STRIP_TAC >| (* 2 sub-goals here *) 251 CONJ_TAC >| (* 2 sub-goals here *) [all...] |
H A D | ContractionScript.sml | 64 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 65 >> rpt STRIP_TAC (* 2 sub-goals here *) 84 >> IMP_RES_TAC WEAK_TRANS_cases2 (* 2 sub-goals here *) 109 >> rpt STRIP_TAC (* 4 sub-goals here *) 126 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) (* 2 sub-goals here *) 179 NTAC 2 GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 187 HO_MATCH_MP_TAC contracts_coind \\ (* co-induction used here! *) 258 >> rpt STRIP_TAC (* 8 sub-goals here *) 274 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) (* 2 sub-goals here *) 296 (* This proof depends on `contracts_IMP_WEAK_EQUIV`, that's why it's here *) [all...] |
H A D | CongruenceScript.sml | 78 >> REPEAT STRIP_TAC (* 7 sub-goals here *) 149 Cases_on `p` (* 8 sub-goals here *) 163 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *) 165 (ONCE_REWRITE_RULE [CONTEXT_cases])) (* 7 sub-goals here *) 171 Cases_on `p` (* 8 sub-goals here *) 187 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *) 189 (ONCE_REWRITE_RULE [CONTEXT_cases])) (* 7 sub-goals here *) 195 Cases_on `p` (* 8 sub-goals here *) 219 Cases_on `p` (* 8 sub-goals here *) 243 Cases_on `p` (* 8 sub-goals here *) [all...] |
H A D | StrongEQScript.sml | 197 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 211 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 213 IMP_RES_TAC TRANS_SUM \\ (* 2 sub-goals here *) 220 IMP_RES_TAC TRANS_SUM \\ (* 2 sub-goals here *) 270 >> CONJ_TAC (* 2 sub-goals here *) 278 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 282 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 288 CONJ_TAC >| (* 2 sub-goals here *) 300 CONJ_TAC >| (* 2 sub-goals here *) 313 CONJ_TAC >| (* 2 sub-goals here *) [all...] |
H A D | WeakEQScript.sml | 106 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 119 >> EQ_TAC (* 2 sub-goals here *) 124 REPEAT STRIP_TAC >- RW_TAC std_ss [] \\ (* 4 sub-goals here, first is easy *) 130 REPEAT STRIP_TAC >| (* 3 sub-goals here *) 199 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 219 >> Cases_on `u` (* 2 sub-goals here *) 292 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 314 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 338 >> EQ_TAC (* 2 sub-goals here *) 341 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) [all...] |
H A D | TraceScript.sml | 101 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 201 >> CONJ_TAC (* 2 sub-goals here *) 207 Cases_on `NULL l` >> FULL_SIMP_TAC std_ss [] >| (* 2 sub-goals here *) 217 Cases_on `NULL l` >> FULL_SIMP_TAC std_ss [] >| (* 2 sub-goals here *) 249 >> CONJ_TAC (* 2 sub-goals here *) 254 Cases_on `l` >> FULL_SIMP_TAC list_ss [] >| (* 2 sub-goals here *) 266 FULL_SIMP_TAC list_ss [FRONT_DEF, LAST_DEF] >| (* 2 sub-goals here *) 282 >> CONJ_TAC (* 2 sub-goals here *) 285 rpt STRIP_TAC >| (* 2 sub-goals here *) 446 >> rpt GEN_TAC >> EQ_TAC (* 2 sub-goals here *) [all...] |
H A D | ExpansionScript.sml | 48 EQ_TAC (* 2 sub-goals here *) 51 REPEAT STRIP_TAC >| (* 3 sub-goals here *) 55 RES_TAC >| (* 2 sub-goals here *) 66 REPEAT STRIP_TAC >> RES_TAC >| (* 5 sub-goals here *) 89 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 90 >> rpt STRIP_TAC (* 2 sub-goals here *) 112 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 113 >> rpt STRIP_TAC (* 2 sub-goals here *) 155 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 171 (ASSUME ``(Exp1 :('a, 'b) simulation) E y``)) (* 2 sub-goals here *) [all...] |
H A D | ObsCongrScript.sml | 61 >> REPEAT STRIP_TAC (* 4 sub-goals here, sharing initial & end tactical *) 74 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 104 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing begin & end tacticals *) 115 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing begin & end tacticals *) 164 >> Cases_on `u` (* 2 sub-goals here *) 176 IMP_RES_TAC (MATCH_MP OBS_CONGR_EPS (* lemma 1 used here *) 212 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 215 IMP_RES_TAC (MATCH_MP OBS_CONGR_WEAK_TRANS (* lemma 2 used here *) 222 IMP_RES_TAC (MATCH_MP OBS_CONGR_WEAK_TRANS (* lemma 2 used here *) 231 >> REPEAT STRIP_TAC (* 3 sub-goals here *) [all...] |
H A D | UniqueSolutionsScript.sml | 39 >> COUNT_TAC (rpt STRIP_TAC) (* 6 sub-goals here *) 46 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 56 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 61 CONJ_TAC >| (* 2 sub-goals here *) 71 CONJ_TAC >| (* 2 sub-goals here *) 81 CONJ_TAC >| (* 2 sub-goals here *) 88 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 126 >> BETA_TAC >> STRIP_TAC (* 2 sub-goals here *) 127 >- (POP_ASSUM MP_TAC >> RW_TAC std_ss [] >| (* 2 sub-goals here *) 149 IMP_RES_TAC STRONG_UNIQUE_SOLUTION_LEMMA \\ (* lemma used here *) [all...] |
H A D | BisimulationUptoScript.sml | 63 >> EQ_TAC (* 2 sub-goals here *) 84 >> RES_TAC (* 2 sub-goals here *) 97 >> rpt STRIP_TAC (* 2 sub-goals here *) 261 >> rpt STRIP_TAC (* 4 sub-goals here *) 288 >> EQ_TAC (* 2 sub-goals here *) 307 >> EQ_TAC (* 2 sub-goals here *) 328 >> RES_TAC (* 4 sub-goals here *) 353 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 354 >> rpt STRIP_TAC (* 2 sub-goals here *) 438 >> IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_EPS (* lemma 1 used here *) [all...] |
H A D | CCSScript.sml | 565 >> EQ_TAC (* 2 sub-goals here *) 570 STRIP_TAC >| (* 2 sub-goals here *) 587 >> EQ_TAC (* 2 sub-goals here *) 607 IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *) 621 IMP_RES_TAC TRANS_SUM >| (* 4 sub-goals here *) 634 >> EQ_TAC (* 2 sub-goals here *) 675 rpt GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 678 IMP_RES_TAC PAR_cases >| (* 3 sub-goals here *) 710 >> IMP_RES_TAC TRANS_PAR (* 3 sub-goals here *) 741 >> EQ_TAC >| (* two goals here *) [all...] |
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | mergeGrammarsBScript.sml | 4 what is being tested here
|
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/ |
H A D | CutFreeScript.sml | 239 >> EQ_TAC (* 2 sub-goals here *) 662 >> REPEAT STRIP_TAC (* 2 sub-goals here, first one is easy *) 674 >> REPEAT STRIP_TAC (* 2 sub-goals here, first one is easy *) 685 >> REPEAT STRIP_TAC (* 2 sub-goals here, first one is easy *) 697 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 703 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 752 >> REPEAT STRIP_TAC (* 9 sub-goals here *) 758 CONJ_TAC >| (* 2 sub-goals here *) 770 CONJ_TAC >| (* 2 sub-goals here *) 782 CONJ_TAC >| (* 2 sub-goals here *) [all...] |
H A D | LambekScript.sml | 158 Note: all theorems here can be simply proved by PROVE_TAC [arrow_rules]. *) 244 >> REPEAT STRIP_TAC (* 7 sub-goals here *) 602 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 609 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 611 ASM_REWRITE_TAC [] >> RES_TAC >| (* 2 sub-goals here *) 615 CONJ_TAC >| (* 2 sub-goals here *) 629 CONJ_TAC >| (* 2 sub-goals here *) 636 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 641 CONJ_TAC >| (* 2 sub-goals here *) 647 ASM_REWRITE_TAC [] >> RES_TAC >| (* 2 sub-goals here *) [all...] |
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | check_keywords.scala | 50 "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | check_keywords.scala | 50 "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Random.sig | 17 [generator] is the type of random number generators, here the
|
/seL4-l4v-master/isabelle/src/Doc/Prog_Prove/document/ |
H A D | svmono.cls | 644 % the upright forms are defined here as \var<Character>
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Prog_Prove/document/ |
H A D | svmono.cls | 644 % the upright forms are defined here as \var<Character>
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | antiquote.scala | 54 Position.here(Position.Line(next.pos.line)))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | antiquote.scala | 54 Position.here(Position.Line(next.pos.line)))
|