/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibClauseset.sig | 12 type filter = {subsumption : bool, simplification : int, splitting : bool} type 13 type parameters = {prefactoring : filter, postfactoring : filter} 16 val update_subsumption : (bool -> bool) -> filter -> filter 17 val update_simplification : (int -> int) -> filter -> filter 18 val update_splitting : (bool -> bool) -> filter -> filter 19 val update_prefactoring : (filter [all...] |
H A D | mlibLiteralnet.sml | 70 fun filter pred = function 72 fun filt (_,l) = let val l = List.filter pred l in (length l, l) end 75 ((T.filter pred pos, T.filter pred neg), (filt t, filt f))
|
H A D | mlibSubsume.sml | 29 val ofilter = Option.filter; 138 fun filter pred (SUBSUME {zero,one,many}) = function 142 val zero = S.filter (pred o snd) zero 143 val one = N.filter (pred o snd) one 146 val l = N.filter (not o curry I.member h o fst) l 147 val r = N.filter (not o curry I.member h o fst) r
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | pureSimps.sml | 12 filter = SOME Cond_rewr.mk_cond_rewrs,
|
H A D | combinSimps.sml | 6 name = SOME "COMBIN", convs = [], congs = [], filter = NONE, ac = [],
|
H A D | boolSimps.sml | 35 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []} 52 ac = [], congs = [literal_cong], convs = [], filter = NONE, 86 congs = [literal_cong], filter = NONE, ac = [], dprocs = []}; 100 convs = [], rewrs = [], filter=NONE, ac=[], dprocs=[]} 110 rewrs = [], filter= NONE, ac = [], dprocs=[] 150 rewrs=[],filter=NONE,ac=[],dprocs=[],congs=[]}; 167 ac = [], congs = [let_cong], convs = [], filter = NONE, 273 dprocs = [], filter = NONE, 289 dprocs = [], filter = NONE, 309 convs = [], dprocs = [], filter [all...] |
/seL4-l4v-master/HOL4/tools/quote-filter/ |
H A D | selftest.sml | 3 val _ = system "./quote-filter input temp-output"
|
H A D | mlton-quote-filter.sml | 2 open filter.UserDeclarations 5 val lexer = filter.makeLexer input state
|
/seL4-l4v-master/HOL4/examples/acl2/lisp/obsolete/ |
H A D | filter-forms.csh | 5 set pprint_book = ${ACL2_HOL_LISP}/filter-forms
|
/seL4-l4v-master/l4v/camkes/glue-spec/document/imgs/ |
H A D | Makefile | 17 default: echo.pdf filter.pdf thydeps.pdf
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/ |
H A D | quicksort.ml | 31 [(\(x.l'). filter(curry $> x) l'); 32 (\(x.l'). filter($not o (curry $> x)) l')]);; 59 [(\(x.l'). filter(curry $> x) l'); 60 (\(x.l'). filter($not o (curry $> x)) l')])
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | Set.sml | 15 fun diff (s1, s2) = List.filter (fn x => not (mem (x, s2))) s1 16 fun intersect (s1, s2) = List.filter (fn x => mem (x, s2)) s1
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | LVTermNetFunctorApplied.sml | 11 fun filter P s = function
|
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_canonTools.sml | 16 filter = NONE,
|
/seL4-l4v-master/HOL4/src/tfl/src/test/ |
H A D | tfl_examplesScript.sml | 53 val _ = overload_on("filter", ``FILTER``) 59 qsort(ord,filter($~ o ord x) rst)++[x]++qsort(ord,filter(ord x) rst))`; 98 let ((L1,L2),P) = ((filter($~ o ord x) rst, 99 filter (ord x) rst), 129 ``LENGTH (filter (\y. SUC x <= y) L) <= LENGTH (filter (\y. x <= y) L)``, 134 WF_REL_TAC `measure \(x,L). LENGTH(filter (\y. x <= y) L)` THEN 139 Q.EXISTS_TAC `LENGTH (filter (\y. x <= y) L)` THEN
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | AtomNet.sml | 40 val filter = TermNet.filter; value
|
H A D | LiteralNet.sml | 44 fun filter pred {positive,negative} = function 45 {positive = AtomNet.filter pred positive, 46 negative = AtomNet.filter pred negative};
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | AtomNet.sml | 40 val filter = TermNet.filter; value
|
H A D | LiteralNet.sml | 44 fun filter pred {positive,negative} = function 45 {positive = AtomNet.filter pred positive, 46 negative = AtomNet.filter pred negative};
|
/seL4-l4v-master/HOL4/examples/unification/triangular/nominal/ |
H A D | ntermLib.sml | 7 congs = [], filter = NONE, 16 congs = ths, filter = NONE,
|
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | reg_allocLib.sml | 37 | all_distinct (x::xs) = x :: all_distinct (filter (fn y => x !~ y) xs) 42 fun diff xs ys = filter (fn y => not (mem y ys)) xs 43 fun intersect xs ys = filter (fn y => mem y xs) ys 80 val vs = filter (fn x => type_of x = ``:word32``) (free_vars tm) 88 val vs = filter (fn x => type_of x = ``:word32``) (free_vars tm) 107 fun partition p xs = filter p xs @ filter (not o p) xs 150 (filter (fn x => not (mem x [#"0",#"1",#"2",#"3",#"4",#"5",#"6",#"7",#"8",#"9",#"'"])) (tl ii) = []) 192 val xs = filter (fn x => x !~ subst m x) (dest_tuple tm) 199 val aux = filter (f [all...] |
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | latex.scala | 160 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) 167 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result) 169 filter(rest, (msg, Position.none) :: result) 170 case _ :: rest => filter(rest, result) 175 filter(Line.logical_lines(root_log), Nil)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | latex.scala | 160 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) 167 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result) 169 filter(rest, (msg, Position.none) :: result) 170 case _ :: rest => filter(rest, result) 175 filter(Line.logical_lines(root_log), Nil)
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_rulesLib.sml | 112 filter (fn x => substring(fst x, 0, 3) = "ARM") (theorems "arm_rules"); 114 fun RULE_FIND m l = filter (can (MATCH_ARM_RULE m)) l; 116 fun RULE_GET m l = filter (fn x => not (term_eq (concl x) T))
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_encodeLib.sml | 47 val (_,(y,z)) = hd (filter (fn y => (fst y = x)) instructions) 59 | all_distinct (x::xs) = x::all_distinct (filter (fn y => not ((x:string) = y)) xs) 61 val i = filter (fn x => not (mem x ["bt","bf"])) i
|