| /seL4-l4v-10.1.1/HOL4/src/finite_map/ |
| H A D | finite_mapSyntax.sml | 85 fun strip acc t = function
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | term_pp_utils.sml | 203 fun strip acc t = let function
|
| H A D | Absyn.sml | 192 let fun strip tm accum = function
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolpp.sml | 108 fun strip n acc tm = function
|
| /seL4-l4v-10.1.1/HOL4/src/monad/ |
| H A D | parmonadsyntax.sml | 240 fun strip acc t = function
|
| H A D | monadsyntax.sml | 284 fun strip acc t = function
|
| /seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
| H A D | pred_setSyntax.sml | 144 fun strip tm = function
|
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | pairSyntax.sml | 292 fun strip dest = function
|
| H A D | PairRules.sml | 1546 fun strip [] = K [] function
|
| /seL4-l4v-10.1.1/HOL4/src/lite/ |
| H A D | liteLib.sml | 123 let fun strip x acc = function
204 fun strip tm = function
215 fun strip tm = function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibArbnum.sml | 60 fun strip [] = [] function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
| H A D | Arbnumcore.sml | 65 fun strip [] = [] function
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Formula.sml | 139 fun strip n (Not fm) = strip (n + 1) fm function
151 fun strip cs (And (p,q)) = strip (p :: cs) q function
174 fun strip cs (Or (p,q)) = strip ( function
197 fun strip cs (Iff (p,q)) = strip (p :: cs) q function
227 fun strip vs (Forall (v,b)) = strip (v :: vs) b function
246 fun strip vs (Exists (v,b)) = strip (v :: vs) b function
[all...] |
| H A D | Term.sml | 354 fun strip tms tm = function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Formula.sml | 139 fun strip n (Not fm) = strip (n + 1) fm function
151 fun strip cs (And (p,q)) = strip (p :: cs) q function
174 fun strip cs (Or (p,q)) = strip ( function
197 fun strip cs (Iff (p,q)) = strip (p :: cs) q function
227 fun strip vs (Forall (v,b)) = strip (v :: vs) b function
246 fun strip vs (Exists (v,b)) = strip (v :: vs) b function
[all...] |
| H A D | Term.sml | 354 fun strip tms tm = function
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | boolSyntax.sml | 223 fun strip A M = function
234 fun strip A M = function
245 fun strip A M = function
|
| H A D | Drule.sml | 692 fun strip [] _ = [] (* Returns a list of (pat,ob) pairs. *) function
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | listSyntax.sml | 243 let fun strip A M = function
255 let fun strip A M = function
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | HolKernel.sml | 116 fun strip A [] = rev A function
131 fun strip A tm = function
151 fun strip A tm = function
184 fun strip acc ty = function
195 fun strip rands M = function
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 343 fun strip (a, ty) = function
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | InductiveDefinition.sml | 65 let fun strip(n,tm,acc) = function
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lzPairRules.sml | 1569 fun strip [] = K [] function
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | ind_types.sml | 93 let fun strip x acc = function
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | functionEncodeLib.sml | 3763 fun strip x y = function
|