Searched refs:prevs (Results 1 - 6 of 6) sorted by last modified time

/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dlinear_set.scala32 start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
47 if (contains(elem)) prevs.get(elem)
65 nexts + (elem -> elem1), prevs + (elem1 -> elem))
73 nexts + (elem1 -> elem), prevs + (elem -> elem1))
77 prevs + (elem2 -> elem) + (elem -> elem1))
95 new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
106 new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
110 prevs - elem2 + (elem3 -> elem1))
152 def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dlinear_set.scala32 start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
47 if (contains(elem)) prevs.get(elem)
65 nexts + (elem -> elem1), prevs + (elem1 -> elem))
73 nexts + (elem1 -> elem), prevs + (elem -> elem1))
77 prevs + (elem2 -> elem) + (elem -> elem1))
95 new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
106 new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
110 prevs - elem2 + (elem3 -> elem1))
152 def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
/seL4-l4v-10.1.1/graph-refine/
H A Dtrace_refute.py635 prevs = [arg[5:] for arg in args if arg.startswith ('prev:')] variable
656 (new, _) = refute (args[0], args[1], prevs,
H A Dstack_logic.py866 prevs = set ([f for f in functions
868 for f in prevs - group:
H A Drep_graph.py392 prevs = self.prevs (n_vc)
394 prevs = [p for p in prevs
401 if not prevs:
403 n_vc = prevs[0]
576 prevs = [n_vc for n_vc in self.prevs (n_vc2)
578 assert len (prevs) <= 1
580 for n_vc in prevs]
1021 def prevs (self, (n, vcount)): member in class:GraphSlice
[all...]
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DCache.sml42 val prevs = Redblackmap.find (cvalue cache, tm) value
48 (case snd (first ok prevs) of
60 c_insert cache (tm, (curr,NONE)::prevs);
64 c_insert cache (tm,(curr,SOME thm)::prevs);
283 val prevs = Redblackmap.find (cvalue cache, t) handle NotFound => [] value
288 case List.find oksome prevs of
336 case List.find oknone prevs of
353 c_insert cache (t, (glhyps,SOME th)::prevs);
362 c_insert cache (t, (glhyps, NONE)::prevs);

Completed in 74 milliseconds