Searched refs:here (Results 76 - 100 of 374) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexExecutableScript.sml13 (* here, we use the datatype from regexDatatypes.Reg_datatype_quot *)
/seL4-l4v-master/HOL4/src/TeX/
H A Dselftest.sml24 called; tests here are at least somewhat a test of its functionality too. *)
/seL4-l4v-master/HOL4/src/coretypes/
H A DpairLib.sml17 gen_new_specification. This occurs here because the derivation
/seL4-l4v-master/HOL4/src/holyhammer/
H A DhhTptp.sml20 by rename_bvarl. There is no need to escape them again here. *)
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaShell.sml115 within conditional guards. There's a lot of faff happening here:
/seL4-l4v-master/HOL4/src/portableML/mosml/
H A DPrettyImpl.sml90 else (* We don't need to break here. *)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DctlSyntax.sml122 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 DExportTree.sml80 its predecessor returns here. *)
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/Examples/
H A DmlEdit.sml152 (* 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 DWord32In64.sml41 (* We can use Word here because a 63-bit tagged value is sufficient. *)
H A DWord32InLargeWord64.sml30 We have to use LargeWord here because Word is only 31-bits. *)
H A DExnPrinter.581.sml73 (* Print a ref. Because refs can form circular structures we include a check for a loop here. *)
H A DExnPrinter.sml73 (* Print a ref. Because refs can form circular structures we include a check for a loop here. *)
H A DString.sml131 (* 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 DFinalPolyML.sml689 (* 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 Dintro.tex65 limitations that we make explicit here.
/seL4-l4v-master/l4v/misc/regression/
H A Drun_tests.py307 # 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 DEXPORT_PARSETREE.sml385 (* 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 Dposition.scala133 /* here: user output */
135 def here(props: T, delimited: Boolean = true): String =
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dposition.scala133 /* here: user output */
135 def here(props: T, delimited: Boolean = true): String =
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dafp.scala103 error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dafp.scala103 error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
/seL4-l4v-master/HOL4/examples/decidable_separationLogic/doc/
H A Dds.tex105 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 DprobScript.sml296 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 DCODETREE_SIMPLIFIER.sml393 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...]

Completed in 188 milliseconds

1234567891011>>