/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
H A D | hh_tac.ml | 126 if is_var hop then if mem hop bnd then (cmin, vmin) 143 if is_var op then try assoc (fst (dest_var op)) vmin with _ -> 0 else failwith "fol_conv_assoc";; 253 if is_var tm then sofar else fn (dest_const tm) sofar;; 346 else if is_var tm || is_const tm then failwith "find_lambda" 355 else if is_var tm || is_const tm then rEFL tm else 388 else if is_var tm || is_const tm then failwith "find_lambda" 397 else if is_var tm || is_const tm then rEFL tm else
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 110 (is_var l1 andalso is_var l2) 180 (all is_var col_i) orelse 181 (all (fn p => Literal.is_literal p orelse is_var p) col_i) orelse 182 (all (fn p => not (Literal.is_pure_literal p) andalso not (is_var p)) col_i) 207 if all is_var col0 (* column 0 is all variables *) 215 val (litpats, varpats) = Lib.partition (not o is_var) lits 332 val globals = (if is_var R then [R] else [])@pat_vars@SV 469 fun var_pure theta = Lib.all (fn {redex,residue} => is_var residue) theta; 574 in if is_var t [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/ |
H A D | exor32.ml | 89 andalso all is_var (strip_pair(rand tm))
|
/seL4-l4v-10.1.1/HOL4/src/combin/ |
H A D | combinSyntax.sml | 103 if is_var s then (f,fst(dest_var s),args)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | export_codeLib.sml | 15 val vs = map (fn (x,y) => (if is_var x then ``0:num`` else cdr (cdr x),y)) vs
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | export_codeLib.sml | 15 val vs = map (fn (x,y) => (if is_var x then ``0:num`` else cdr (cdr x),y)) vs
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | export_codeLib.sml | 18 val vs = map (fn (x,y) => (if is_var x then ``0:num`` else
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | intSimps.sml | 103 if is_var tm then true 240 | NONE => if is_var t then if HOLset.member(bnds, t) then acc
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | Witness.sml | 59 fun is_lit x = (is_const x) orelse (is_var x); 70 else if is_var tm then
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Gen_arith.sml | 40 if (is_var tm) then true 110 fun is_num_var tm = is_var tm andalso type_of tm = num_ty
|
H A D | numSimps.sml | 438 | NONE => if is_var t then if HOLset.member(bnds, t) then acc 548 val lsucs = find_terms (fn t => is_suc t andalso is_var (rand t)) l 573 val lsucs = find_terms (fn t => is_suc t andalso is_var (rand t)) l 574 val v = rand (valOf (List.find (is_var o rand) lsucs))
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Opening.sml | 104 (if (is_var (rand tm) andalso mem (rand tm) genvars) 139 fun reprocess_flag assum = if is_var assum then false else true;
|
H A D | Cond_rewr.sml | 303 not (is_var t) orelse type_of t <> bool orelse 330 else if is_var n andalso not (n IN hypfvs) then 359 else if is_var conc andalso not (conc IN hypfvs) then
|
/seL4-l4v-10.1.1/HOL4/examples/misc/ |
H A D | wardScript.sml | 234 listSyntax.is_nil res2 andalso List.all is_var pfx1 andalso 235 List.all is_var sfx1
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | regAlloc.sml | 68 (* is_var exp andalso *) 162 if is_var x then (x |-> find_pos (regenv, x)) :: ys 220 if is_var x then (x |-> find_reg (regenv, x)) :: ys 274 if is_var exp 464 else if is_var M andalso is_mem M then
|
H A D | basic.sml | 29 is_var t orelse is_word_literal t orelse
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernel.sml | 510 if is_var vtm then let 541 if is_var vhop andalso not (HOLset.member (lconsts, vhop)) andalso 586 val (realinsts, patterns) = partition (is_var o #redex) insts 660 if is_var vtm then 697 (if is_var p then p
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | binderLib.sml | 159 if is_var t then 167 val strings = List.filter (fn t => is_var t orelse is_string_literal t) 169 val stringsets = List.filter is_var (find_terms (eqty stringset_ty) t) 186 fun filterthis t = not (is_var t) orelse mem t finite_sets 314 case List.find (not o is_var) args of
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairLib.sml | 120 if is_var vs
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhTptp.sml | 41 else if is_var tm then tptp_of_var arity tm
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibTerm.sig | 33 val is_var : term -> bool value
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | FinalTerm-sig.sml | 49 val is_var : term -> bool value
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttTools.sml | 360 else if is_var t1 andalso is_var t2 then Term.compare (t1,t2) 361 else if is_var t1 then LESS 362 else if is_var t2 then GREATER
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_compilerLib.sml | 84 | ends (FUN_VAL t) = if is_var t orelse pairSyntax.is_pair t then [t] else []
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | prog_ppcLib.sml | 52 val mems = filter (is_var o cdr o cdr) mems 99 fun g th tm tm' = if is_var tm then INST [ tm |-> tm' ] th else th
|