| /seL4-l4v-master/HOL4/examples/bootstrap/ |
| H A D | codegen_proofsScript.sml | 122 fun strip tm = tm |> ASSUME |> SIMP_RULE std_ss [PULL_FORALL] |> SPEC_ALL |> concl function
|
| /seL4-l4v-master/HOL4/src/finite_maps/ |
| H A D | finite_mapSyntax.sml | 85 fun strip acc t = function
|
| /seL4-l4v-master/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-master/HOL4/src/monad/ |
| H A D | parmonadsyntax.sml | 240 fun strip acc t = function
|
| H A D | monadsyntax.sml | 327 fun strip acc t = function
|
| /seL4-l4v-master/HOL4/src/bool/ |
| H A D | boolpp.sml | 112 fun strip n acc tm = function
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Ho_Rewrite.sml | 243 fun strip t = function
|
| H A D | boolSyntax.sml | 225 fun strip A M = function
236 fun strip A M = function
247 fun strip A M = function
|
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | pred_setSyntax.sml | 144 fun strip tm = function
|
| /seL4-l4v-master/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-master/HOL4/src/metis/ |
| H A D | mlibArbnum.sml | 60 fun strip [] = [] function
|
| /seL4-l4v-master/HOL4/src/portableML/mosml/ |
| H A D | Arbnumcore.sml | 65 fun strip [] = [] function
|
| /seL4-l4v-master/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-master/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-master/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-master/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-master/HOL4/src/postkernel/ |
| H A D | HolKernel.sml | 116 fun strip A [] = rev A function
133 fun strip A tm = function
153 fun strip A tm = function
186 fun strip acc ty = function
197 fun strip rands M = function
[all...] |
| /seL4-l4v-master/HOL4/src/IndDef/ |
| H A D | InductiveDefinition.sml | 65 let fun strip(n,tm,acc) = function
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 340 fun strip (a, ty) = function
|
| /seL4-l4v-master/HOL4/src/real/ |
| H A D | realSimps.sml | 788 fun strip A t = function
862 fun strip A t = function
|
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | lzPairRules.sml | 1569 fun strip [] = K [] function
|