/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/ |
H A D | regexExecutableScript.sml | 13 (* here, we use the datatype from regexDatatypes.Reg_datatype_quot *)
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | selftest.sml | 24 called; tests here are at least somewhat a test of its functionality too. *)
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | pairLib.sml | 17 gen_new_specification. This occurs here because the derivation
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | hhTptp.sml | 20 by rename_bvarl. There is no need to escape them again here. *)
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | OmegaShell.sml | 115 within conditional guards. There's a lot of faff happening here:
|
/seL4-l4v-master/HOL4/src/portableML/mosml/ |
H A D | PrettyImpl.sml | 90 else (* We don't need to break here. *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | ctlSyntax.sml | 122 val ksPu = inst [alpha |-> p_ty,beta |-> s_ty] ksPu_tm (* FIXME: why are alpha and beta inverted here? *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | ExportTree.sml | 80 its predecessor returns here. *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/Examples/ |
H A D | mlEdit.sml | 152 (* Menu selections arrive here. *) 349 NONE => (* No breaks on the line - break just before here. *) 356 then (* End of line - stop here. *) 568 val pictureId = 1000 (* Could use any number here. *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Word32In64.sml | 41 (* We can use Word here because a 63-bit tagged value is sufficient. *)
|
H A D | Word32InLargeWord64.sml | 30 We have to use LargeWord here because Word is only 31-bits. *)
|
H A D | ExnPrinter.581.sml | 73 (* Print a ref. Because refs can form circular structures we include a check for a loop here. *)
|
H A D | ExnPrinter.sml | 73 (* Print a ref. Because refs can form circular structures we include a check for a loop here. *)
|
H A D | String.sml | 131 (* There's an irritating dependency here. Char uses StringCvt.reader 256 we still check it here in unsignedShortOrRaiseSize. *) 340 else if p (sub(s, i)) (* TODO: We don't need sub to do the range check here *) 544 if i <= 0 (* unsignedShortOrRaiseSize raises Size if i < 0 which isn't right here. *) 570 if i <= 0 (* unsignedShortOrRaiseSize raises Size if i < 0 which isn't right here. *) 645 the unsafe subscript function here. *) 708 else (* Stop here. *) if res > maxOrd then NONE 808 (* Note: the web page says \u here but it seems it should 1340 string type we can use substring here. *) 1361 (* Since we've already checked the bounds we don't need to do it here [all...] |
H A D | FinalPolyML.sml | 689 (* We use the functional layer and a reference here rather than TextIO.input1 because 691 only one thread accessing the stream so we don't need it here. *) 911 val here = fullName value 920 then (here,"ml_bind") 936 case filePresent (here, kind, name) of 938 | _ => here; 977 (* There was previously a comment about returning NONE here if 1319 an exception here. *) 1443 (* We have a full environment here for future expansion but at 1476 we need to use globals here s [all...] |
/seL4-l4v-master/l4v/camkes/glue-proofs/document/ |
H A D | intro.tex | 65 limitations that we make explicit here.
|
/seL4-l4v-master/l4v/misc/regression/ |
H A D | run_tests.py | 307 # Cancel the timer. Small race here (if the timer fires just after the 331 here = os.path.dirname(os.path.abspath(__file__)) 332 command = [os.path.join(here, 'timeout_output'), test_name]
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | EXPORT_PARSETREE.sml | 385 (* There are three possibilities here. exception exc; exception exc of ty; exception exc = exc' *) 398 name, nameLoc, (* Type could be in here? *)definingLocationProps locations) 411 name, nameLoc, (* Type could be in here? *)definingLocationProps locations) 478 To avoid having nodes that overlap we return only the pattern part here. *)
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | position.scala | 133 /* here: user output */ 135 def here(props: T, delimited: Boolean = true): String =
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | position.scala | 133 /* here: user output */ 135 def here(props: T, delimited: Boolean = true): String =
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | afp.scala | 103 error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | afp.scala | 103 error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
|
/seL4-l4v-master/HOL4/examples/decidable_separationLogic/doc/ |
H A D | ds.tex | 105 The definitions of the fragment of separation logic used here follow mainly the definition in 322 To be close to the \HOL\ formalisation, a list notation is used here as well. 360 considered here. We are mainly interested in checking the validity of 424 The subset of separation logic presented here is very similar to the one used by 428 has been introduced here to help the deep-embedding in $\HOL$. It is a 435 could be easily added to the logic presented here. For sake of time and 508 maximal height of the tree, is used instead of the one used here. That 609 instantiations of the $\sftree$ inference, they won't be explained here. 1100 counterexample for each case. The actual proof is tedious and omitted here. 1255 extend the fragment of separation logic used here an [all...] |
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | probScript.sml | 296 SIGMA_ALGEBRA_SIGMA, SPACE_SUBSETS_PROB_ALGEBRA] (* 3 goals here *) 389 COUNTABLE_IMAGE_NUM] (* 2 sub-goals here *) 637 >> RW_TAC std_ss [PREIMAGE_ALT] (* 3 sub-goals here *) 943 >> EQ_TAC (* 2 sub-goals here *) 1121 BIGUNION_EMPTY, prefix_set_def, UNION_EMPTY] (* 5 goals here *) 1359 RW_TAC std_ss [indep_fn_def, GSPECIFICATION] >| (* 4 goals here *) 1410 IN_IMAGE, IN_UNIV] (* 2 sub-goals here *) 1465 IN_IMAGE, IN_UNIV] (* 2 sub-goals here *) 1684 >> Strip >| (* 2 sub-goals here *) 1895 >> RW_TAC std_ss [] >| (* 2 goals here *) [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_SIMPLIFIER.sml | 393 This is particularly useful with string concatenation. Small here means three or less. 528 (* If this raises an exception stop here. *) 544 (* If this raises an exception stop here. *) 708 (* Have to modify the environment here so that if we look up free variables 771 big. In some cases we can get exponential blow-up. We check here that the 797 big. In some cases we can get exponential blow-up. We check here that the 817 (* We have to make a special check here that we are not passing in the function 848 of the parameters. We need a new table here because the addresses 1312 indexes. We could have silly index values here which will 1363 (* We need callcode_tupled here becaus [all...] |