/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 448 val res2 = value 452 fun res2' th = 455 val th' = res2 th 461 (res1, res2') 1089 val res2 = ski_discrim_unify pos_db (vars', eq2) value 1092 map (extra2 o process vars' eq2) res2
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | alist_treeLib.sml | 351 val res2 = timeit "map extract" (map (extract_test f rs)) (upto 1 1000) value 352 in res2 end
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | stack_analysisLib.sml | 99 val res2 = (pc,assum2,u2,NONE,get_pc_val post2) value 100 in [res1,res2] end handle HOL_ERR _ =>
|
H A D | derive_specsLib.sml | 584 val res2 = map (fn (nn,(th,i,x),y) => value 597 val xs = (diff (assign ~1 (construct_thm_trace res2)) [~1])
|
/seL4-l4v-master/graph-refine/ |
H A D | logic.py | 1442 res2 = set () 1449 res2.add (n) 1450 assert res == res2, (graph, res, res2)
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Portable.sml | 437 fun redres_eq eq1 eq2 {residue=res1,redex=red1} {residue=res2,redex=red2} = 438 eq1 red1 red2 andalso eq2 res1 res2
|
/seL4-l4v-master/HOL4/src/opentheory/compat/ |
H A D | HOL4boolScript.sml | 20 val res2 = export(``~(p ==> q) ==> p``, value
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Pmatch.sml | 470 | res_min (SOME res1) res2 = 471 (case min_fun (res1, res2) of GREATER => res2 | _ => res1)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Normalize.sml | 245 val res2 = polarity f 246 val _ = res1 = res2 orelse raise Bug "polarity" 248 res2
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Normalize.sml | 245 val res2 = polarity f 246 val _ = res1 = res2 orelse raise Bug "polarity" 248 res2
|
/seL4-l4v-master/HOL4/src/boss/ |
H A D | selftest.sml | 107 val res2 = test_assert (equal 2 o length o #1) value
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/spec/ |
H A D | lisp_semanticsScript.sml | 384 ``R_ap x (res,k,io,F) /\ R_ap x (res2,k2,io2,b) ==> ~b``,
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | CooperCore.sml | 1120 val res2 = CHOOSE (y, lemma) res1 value 1122 val res3 = DISJ_CASES disj2_exm positive_disj2 res2
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_grammar.sml | 1115 restr_binders = res2, res_quanop = resq2} = S2 1120 restr_binders = Lib.union res1 res2, res_quanop = resq1}
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
H A D | arm.sml | 4398 val (res1,res2) = SignedParallelAddSub16(op',(n,m)) 4400 ( write'R(BitsN.@@(BitsN.fromInt(res2,16),BitsN.fromInt(res1,16)),d) 4421 if IntInf.>=(res2,0) 4431 val (res1,res2) = SignedParallelAddSub16(op',(n,m)) 4433 ( write'R(BitsN.@@(SignedSat 16 (res2,16),SignedSat 16 (res1,16)),d) 4440 val (res1,res2) = SignedParallelAddSub16(op',(n,m)) 4444 (BitsN.fromInt(IntInf.div(res2,2),16), 4484 val (res1,(res2,(res3,res4))) = SignedParallelAddSub8(sub,(n,m)) 4489 BitsN.fromInt(res2,8),BitsN.fromInt(res1,8)],d) 4504 BitsN.bitFieldInsert(1,1) (w,BitsN.fromBit(IntInf.>=(res2, [all...] |
H A D | armScript.sml | 9554 Let(TP[iVar"res1",iVar"res2"],Var("v",PTy(iTy,iTy)), 9559 TP[CC[Mop(Cast F16,iVar"res2"), 9584 ITE(Bop(Ge,iVar"res2",LI 0), 9600 Let(TP[iVar"res1",iVar"res2"],Var("v",PTy(iTy,iTy)), 9605 TP[iVar"res2",LN 16]),qVar"s"), 9632 Let(TP[iVar"res1",iVar"res2"],Var("v",PTy(iTy,iTy)), 9638 TP[CC[Mop(Cast F16,Bop(Div,iVar"res2",LI 2)), 9687 Let(TP[iVar"res1",iVar"res2",iVar"res3",iVar"res4"], 9695 Mop(Cast F8,iVar"res2"), 9719 Bop(Ge,iVar"res2",L [all...] |
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | ind_rel.sml | 1565 val res2 = delete_conjs1 pred body2 value 1567 val rimp2 = DISCH (fst (dest_imp (concl imp2))) res2
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_opsScript.sml | 65 val res2 = filter (not o can dest_sep_cond) res value 67 val res3 = map dest_comb (filter (not o can dest_sep_hide) res2)
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootLib.sml | 773 val res2 = map (CONV_RULE (RATOR_CONV (RAND_CONV (K (GSYM sfb_thm))))) res value 775 res2
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/monadic-arm/ |
H A D | armScript.sml | [all...] |