| /seL4-l4v-master/HOL4/examples/hardware/hol88/ |
| H A D | binary-trees.ml | 22 % where t1 and t2 are trees. Leaf nodes are labelled with values of % type
[all...] |
| H A D | RESET_PARITY.ml | 86 % | T if f is T an even number of times between t1 and t2% var
88 % | F if f is T an odd number of times between t1 and t2 % var
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | x86_Script.sml | 56 val t2 = Time.now(); value
|
| /seL4-l4v-master/HOL4/src/TeX/ |
| H A D | selftest.sml | 36 val t2 = mk_I(T) value
|
| /seL4-l4v-master/HOL4/examples/CCS/ |
| H A D | ObsCongrLib.sml | [all...] |
| H A D | WeakEQLib.sml | [all...] |
| H A D | MultivariateScript.sml | 734 val t2 = value
780 val t2 = value
1280 val t2 = value
1328 val t2 = value
|
| H A D | StrongEQLib.sml | [all...] |
| H A D | ExampleScript.sml | 147 and t2 = ISPECL [``prefix (label (name "a")) (prefix (label (name "b")) nil)``, value
|
| H A D | WeakLawsConv.sml | [all...] |
| /seL4-l4v-master/HOL4/src/holyhammer/ |
| H A D | hhReconstruct.sml | 67 val t2 = !reconstruction_timeout value
|
| /seL4-l4v-master/HOL4/src/coretypes/ |
| H A D | selftest.sml | 63 val t2 = ``pair_CASE (p:'a # 'b) (\x y. if y = a then x else f x y)`` value
|
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | closure.sml | 115 val t2 = identify_fun body value
|
| H A D | basic.sml | 206 val t2 = trav M2 value
|
| H A D | funcCall.sml | 137 val t2 = regAlloc.parallel_move dst dst0 t1 value
|
| /seL4-l4v-master/HOL4/src/refute/ |
| H A D | AC.sml | 157 val t2 = rand(rator t23) and t3 = rand t23 value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | UTuple.sml | 22 fun t2 (x,y,z) = y function
|
| H A D | gr_t.sml | 161 val t2 = updLabAdj (t1,pred,addLabSuc n) value
172 val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *) value
225 val t2 = M.update (t1,w,addLabPred v l) value
252 val t2 = updAdj (t1,pred,addSuc n) value
261 val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *) value
301 val t2 = M.update (t1,w,addPred v) value
329 val t2 = updLabAdj (t1,pred,addLabSuc n) value
370 val t2 = updAdj (t1,pred,addSuc n) value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | UTuple.sml | 22 fun t2 (x,y,z) = y function
|
| H A D | gr_t.sml | 161 val t2 = updLabAdj (t1,pred,addLabSuc n) value
172 val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *) value
225 val t2 = M.update (t1,w,addLabPred v l) value
252 val t2 = updAdj (t1,pred,addSuc n) value
261 val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *) value
301 val t2 = M.update (t1,w,addPred v) value
329 val t2 = updLabAdj (t1,pred,addLabSuc n) value
370 val t2 = updAdj (t1,pred,addSuc n) value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | UTuple.sml | 22 fun t2 (x,y,z) = y function
|
| H A D | gr_t.sml | 161 val t2 = updLabAdj (t1,pred,addLabSuc n) value
172 val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *) value
225 val t2 = M.update (t1,w,addLabPred v l) value
252 val t2 = updAdj (t1,pred,addSuc n) value
261 val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *) value
301 val t2 = M.update (t1,w,addPred v) value
329 val t2 = updLabAdj (t1,pred,addLabSuc n) value
370 val t2 = updAdj (t1,pred,addSuc n) value
[all...] |
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | selftest.sml | 611 val t2 = `` value
[all...] |
| /seL4-l4v-master/HOL4/help/src-sml/ |
| H A D | Database.sml | 157 val t2 = readTable is value
|
| /seL4-l4v-master/HOL4/src/finite_maps/ |
| H A D | sptreeSyntax.sml | 214 val t2 = sptree_pretty_term t value
[all...] |