Searched refs:here (Results 26 - 50 of 374) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/CCS/
H A DCCSConv.sml268 >> EQ_TAC (* 2 sub-goals here *)
311 >> EQ_TAC (* 2 sub-goals here *)
404 >> EQ_TAC (* 2 sub-goals here *)
407 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
423 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
467 >> EQ_TAC (* 2 sub-goals here *)
470 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
507 >> EQ_TAC (* 2 sub-goals here *)
510 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *)
H A DObsCongrLawsScript.sml294 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
323 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
325 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
364 >> REPEAT STRIP_TAC (* 2 sub-goals here *)
366 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *)
/seL4-l4v-master/HOL4/src/1/
H A DAC_Sort.sig39 NO_CONV are OK here), nothing further is done. If it
/seL4-l4v-master/HOL4/src/HolSat/
H A DsatScript.sml2 (* random theorems used here, there, everywhere by HolSatLib *)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DholCheck.sml15 val _ = if bdd.isRunning() then () else bdd.init 1000000 10000 (* FIXME: allow user to supply the nums here *)
H A DdecompTools.sml61 (*FIXME: I'm being lazy here by assuming empty environments. Generalise this. *)
80 (* other than that, all the args here are from the stuff returned by ksTools.mk_formal_KS *)
115 (* here I am assuming that the rhs of ks1 is just the full rhs of the lifted ks (e.g. apb_h)
116 which is just the lhs of the unlifted ks (talking about the ks_t_def's produced by mk_formal_KS here)
177 (*FIXME: at the moment only the env=EMPTY_ENV will work here *)
/seL4-l4v-master/HOL4/examples/PSL/1.01/standalone/
H A Dpslcheck.sml33 * Arguments have to be in the order shown here.
/seL4-l4v-master/isabelle/src/Pure/Thy/
H A Dsessions.scala108 "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
328 quote(info.name) + Position.here(info.pos))
486 error("Bad theory name " + quote(thy) + Position.here(pos))
495 quote(thy_name) + Position.here(pos))
520 quote(entry.name) + Position.here(entry.pos))
560 quote(name) + Position.here(pos))
567 cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
579 error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
580 Position.here(graph.get_node(info.name).pos))
602 "\n for session " + quote(session1) + Position.here(info
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/
H A Dsessions.scala108 "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
328 quote(info.name) + Position.here(info.pos))
486 error("Bad theory name " + quote(thy) + Position.here(pos))
495 quote(thy_name) + Position.here(pos))
520 quote(entry.name) + Position.here(entry.pos))
560 quote(name) + Position.here(pos))
567 cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
579 error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
580 Position.here(graph.get_node(info.name).pos))
602 "\n for session " + quote(session1) + Position.here(info
[all...]
/seL4-l4v-master/l4v/camkes/glue-spec/document/
H A Dintro.tex19 Although this is its most interesting part, the specification presented here
44 weak memory models. We do not do this here, because the intended application
/seL4-l4v-master/HOL4/src/tfl/examples/sorting/
H A DpartitionScript.sml88 subgoals here, so we have to take round-about measures.
/seL4-l4v-master/HOL4/examples/misc/
H A DcontMonadScript.sml11 What in Haskell is Cont r a here becomes ('a,'r) Cont, where 'r is
/seL4-l4v-master/HOL4/src/coretypes/
H A DDefnBase.sig46 possibly universally quantified equations. The machinery here
/seL4-l4v-master/seL4/manual/parts/
H A Dintro.tex9 % FIXME: Use of service, mechanism and abstraction is munged through here and the rest of the manual
/seL4-l4v-master/HOL4/polyml/basis/
H A DLibrarySupport.sml97 and Word8Array.vector (= Word8Vector.vector) here so that they
105 (* Using the Array constructor here does not add any overhead since it is compiled
110 define it as "string" here so that it inherits the same equality function.
224 (* The onEntry list. PolyML.onEntry adds a mutex here. *)
H A DThreadLib.sml27 defined here using the underlying calls. The original version with
H A DIEEEReal.sml47 much safer to map them to known values here. *)
49 raised here in the event of an error. convReal in the Real
123 space here so return NONE if we find any. *)
/seL4-l4v-master/HOL4/src/relation/
H A DbisimulationScript.sml80 HO_MATCH_MP_TAC BISIM_REL_coind \\ (* co-induction used here! *)
295 >> RES_TAC (* 8 sub-goals here, the same last tactic *)
324 HO_MATCH_MP_TAC WBISIM_REL_coind \\ (* co-induction used here! *)
/seL4-l4v-master/HOL4/src/portableML/
H A DRedblackset.sml209 in (* FIXME: here is lots of room for optimizations *)
242 in (* FIXME: here is lots of room for optimizations *)
261 in (* FIXME: here is lots of room for optimizations *)
286 in (* FIXME: here is lots of room for optimizations *)
312 in (* FIXME: here is lots of room for optimizations *)
/seL4-l4v-master/isabelle/src/Pure/System/
H A Doptions.scala313 error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
314 Position.here(other.pos))
324 Position.here(pos))
/seL4-l4v-master/l4v/isabelle/src/Pure/System/
H A Doptions.scala313 error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
314 Position.here(other.pos))
324 Position.here(pos))
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dresources.scala204 " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
211 error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
312 Dependencies.required_by(initiators) + Position.here(pos)
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/
H A Dresources.scala204 " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
211 error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
312 Dependencies.required_by(initiators) + Position.here(pos)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DPretty.sml50 (* This is complicated because the data structures we use here will be exported into
53 compiling this code. We use an explicit representation here which must be kept in
210 else (* We don't need to break here. *)
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/
H A DExampleScript.sml207 >> CONJ_TAC (* 2 sub-goals here *)
218 CONJ_TAC >| (* 2 sub-goals here *)
248 >> CONJ_TAC (* 2 sub-goals here *)
256 CONJ_TAC >| (* 2 sub-goals here *)

Completed in 343 milliseconds

1234567891011>>