| /seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
| H A D | Nat.sig | 31 val pred: nat -> nat value
|
| H A D | Nat.sml | 54 fun pred n = n - one function
|
| /seL4-l4v-master/HOL4/src/pred_set/Manual/ |
| H A D | description.tex | [all...] |
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | PSet_ind.sml | 66 val pred = mk_abs(sv,subst [s |-> sv] conc) value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | gr-sig.sml | 79 val pred : node * ('a,'b) graph -> node list value
122 val pred : node * 'a graph -> node list value
|
| H A D | gr_t.sml | 133 fun pred _ = raise NotImplemented function
197 fun pred g = map p2 (p2 (bwd g)) function
273 fun pred g = p2 (bwd g) function
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | gr-sig.sml | 79 val pred : node * ('a,'b) graph -> node list value
122 val pred : node * 'a graph -> node list value
|
| H A D | gr_t.sml | 133 fun pred _ = raise NotImplemented function
197 fun pred g = map p2 (p2 (bwd g)) function
273 fun pred g = p2 (bwd g) function
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | gr-sig.sml | 79 val pred : node * ('a,'b) graph -> node list value
122 val pred : node * 'a graph -> node list value
|
| H A D | gr_t.sml | 133 fun pred _ = raise NotImplemented function
197 fun pred g = map p2 (p2 (bwd g)) function
273 fun pred g = p2 (bwd g) function
[all...] |
| /seL4-l4v-master/HOL4/src/0/ |
| H A D | Net.sml | 185 fun pred (x,_) = (x=label) function
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Ho_Rewrite.sig | 39 type pred = term -> bool type
|
| H A D | Rewrite.sig | 52 type pred = term -> bool type
|
| H A D | Rewrite.sml | 20 type pred = term -> bool type
|
| H A D | Ho_Rewrite.sml | 17 type pred = term -> bool; type
233 val (pred,(th,beta_fn)) = op_assoc aconv pat ass_list value
|
| /seL4-l4v-master/HOL4/src/datatype/ |
| H A D | ind_typeScript.sml | 183 let val (pred, witness) = dest_comb(concl thm) value
|
| /seL4-l4v-master/HOL4/src/experimental-kernel/ |
| H A D | Net.sml | 182 fun pred (x,_) = (x=label) function
|
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | FCNet.sml | 173 fun pred (x,_) = (x=label) function
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Proof.sml | 112 fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl function
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Proof.sml | 112 fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl function
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibModel.sml | 69 fun pred x = case pred1 x of NONE => pred2 x | sb => sb function
97 fun pred ("<>",[m,n]) = SOME (m = n) function
129 fun pred ("<=",[m,n]) = SOME (m <= n) function
158 fun pred ("<=",[m,n]) = SOME (m <= n) function
188 fun pred ("in",[_,n]) = function
[all...] |
| /seL4-l4v-master/HOL4/polyml/basis/ |
| H A D | StringSignatures.sml | 31 val pred : char -> char value
|
| /seL4-l4v-master/HOL4/examples/AI_tasks/ |
| H A D | mleDiophProve.sml | 22 val pred = mk_var ("p",``:num -> bool``) value
|
| /seL4-l4v-master/HOL4/src/num/ |
| H A D | numLib.sml | 92 val pred = rand lc value
|
| /seL4-l4v-master/HOL4/src/res_quan/src/ |
| H A D | res_quanLib.sml | 103 val (pred,v) = dest_comb ante value
|