Searched refs:is_var (Results 1 - 25 of 178) sorted by path

12345678

/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A DarmLib.sml70 fun fix_condition tm = if is_var tm then condition_to_word4 tm else tm
H A Darm_disassemblerLib.sml180 if Term.is_var tm then
801 val v2 = opt (is_var cond orelse is_PC cond) "2"
H A Darm_encoderLib.sml482 if is_var cond orelse is_AL cond then
876 if is_var cond orelse is_AL cond then
1441 (mk_word4 (if is_var cond orelse is_PC cond then 15 else 14),i)
H A Darm_parserLib.sml758 (is_var tm orelse word_lower_same (tm,mk_word4 7));
1735 if is_var i then
1777 if is_var i then
1785 if is_var cond orelse is_AL cond then
1789 val wide_okay = if is_var cond orelse is_AL cond then
1822 (if is_var i then
1841 if is_var i then
1881 (if is_var i then
1903 (if is_var i then
1951 if is_var
[all...]
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DDerivedBddRules.sml154 if is_var tm
159 if is_var tm' then BddVar false vm tm' else BddNot(recfn tm')
H A DPrimitiveBddRules.sml137 if is_var v andalso type_of v = bool
270 if not(is_var v)
273 if not(is_var v')
339 if is_var v andalso Varmap.eq(vm,vm1) andalso Varmap.eq(vm1,vm2)
373 if not(is_var v)
468 if not(is_var v)
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DbddTools.sml206 in List.map (fn v => if is_var v then T else v) t1 end;
H A DcommonTools.sml148 fun is_bool_var v = is_var v andalso (Type.compare(type_of v,bool)=EQUAL)
H A DlzConv.sml458 if is_var arg_t then
1292 if not(is_var v)
1404 if not(is_var x)
H A DlzPairRules.sml36 if is_var p then ABS p th
242 if is_var p then BETA_CONV tm
270 if is_var p
279 if is_var bp
282 if is_var np
344 if is_var tm then mem tm V else
374 fun new_pair p s = if is_var p then new_var p s else let val (p1,p2) = dest_pair p in mk_pair(new_pair p1 s,new_pair p2 s) end
392 in if is_var np
393 then if is_var opr then ALPHA_CONV np tm
403 if is_var op
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/
H A DmatcherScript.sml45 val assumer = if is_var l then K ALL_TAC else ASSUME_TAC
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dsexp.sml1045 if is_var tm
1114 if is_var opr
1187 if is_var tm then fst(dest_var tm)
1809 if is_var tm
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dsexp.sml971 if is_var tm
1040 if is_var opr
1113 if is_var tm then fst(dest_var tm)
1735 if is_var tm
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A Dacl2encodeLib.sml1240 val pvars = filter is_var (mapfilter (rand o rator) coders)
H A DencodeLib.sml901 val vars = filter is_var hfuns
1733 (if is_var (rand (rhs g)) then
H A DfunctionEncodeLib.sml133 orelse (is_var ratort andalso
152 else if (is_var ratort andalso
1275 is_var (RHS (concl thm))
1631 else if is_var f1 andalso is_var f2
1752 if all (all is_var o snd o strip_comb) constructors andalso
1820 val _ = if is_var a then () else
2090 val _ = if exists (not o is_var) vars then
2121 if is_var term then mk_var(fst (dest_var term),t) else raise e;
2472 (is_var
[all...]
H A DpolytypicLib.sml509 val _ = assert "GEN_THM" [("List is not a list of variables",all is_var)] list
625 val all_vars = find_terms is_var term
1043 val _ = assert' [("Function list is not a list of variables",all is_var)] fvs
H A Dsexp.sml971 if is_var tm
1040 if is_var opr
1113 if is_var tm then fst(dest_var tm)
1735 if is_var tm
H A DtranslateLib.sml35 (if is_var fx' then (subst [inst_it fx' fy' fx' |-> fy'])
37 else (if is_var fy' then (subst [inst_it fy' fx' fy' |-> fx'] o inst_it fy' fx') else raise match)))
39 | (fy,[]) => if is_var fy then subst [inst_it fy t1 fy |-> t1] o inst_it fy t1 else raise match)
41 if is_var fx then (subst [inst_it fx t2 fx |-> t2]) else
42 (if same_const fx t2 then I else (if is_var t2 then (subst [inst_it t2 fx t2 |-> fx] o inst_it t2 fx) else raise match))
77 if is_var (var thm)
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/
H A DNOT32.ml56 andalso all is_var (strip_pair(rand tm))
H A Dexor32.ml89 andalso all is_var (strip_pair(rand tm))
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A Dcompile.sml139 else if null(free_vars t) orelse is_var t
497 is_var tm
1198 if is_var t then applysubst theta t else
1374 if is_var vs
1554 else if is_var bdy andalso can (assoc bdy) args_match
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DANF.sml136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t
H A DIR.sml189 if is_var exp then
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DANF.sml136 else if is_var t orelse is_word_literal t orelse numSyntax.is_numeral t orelse is_const t

Completed in 290 milliseconds

12345678