| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_opsScript.sml | 374 val result = prove_spec th imp def pre_tm post_tm value
419 val result = prove_spec th imp def pre_tm post_tm value
464 val result = prove_spec th imp def pre_tm post_tm value
491 val result = prove_spec th imp def pre_tm post_tm value
532 val result = prove_spec th imp def pre_tm post_tm value
573 val result = prove_spec th imp def pre_tm post_tm value
601 val result = prove_spec th imp def pre_tm post_tm value
641 val result = prove_spec th imp def pre_tm post_tm value
675 val result = prove_spec th imp def pre_tm post_tm value
705 val result = prove_spec th imp def pre_tm post_tm value
726 val result = prove_spec th imp def pre_tm post_tm value
763 val result = prove_spec th imp def pre_tm post_tm value
787 val result = prove_spec th imp def pre_tm post_tm value
828 val result = prove_spec th imp def pre_tm post_tm value
853 val result = prove_spec th imp def pre_tm post_tm value
1229 val result = prove_spec th imp def pre_tm post_tm value
1252 val result = prove_spec th imp def pre_tm post_tm value
1681 val result = prove_spec th imp def pre_tm post_tm value
1682 val result = RW [GSYM zLISP_raw] result value
1737 val result = prove_spec th imp def pre_tm post_tm value
1738 val result = RW [GSYM zLISP_raw] result value
1790 val result = prove_spec th imp def pre_tm post_tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lzPairRules.sml | 1403 val result = list_mk_pforall ([x,y],bod) value
1429 val result = list_mk_pexists ([x,y],bod) value
1455 val result = mk_pforall (xy,bod) value
1482 val result = mk_pexists (xy,bod) value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Prim_rec.sml | 1710 val result = GEN_ALL (MATCH_MP IMP_F result1) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 155 val result = dest_tuple (hd res) value
765 val result = tree_composition (th,the i,thms,entry,exit,conds,false) value
1848 val result = if (get_abbreviate_code()) then result value
1872 val result = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 678 val result = MP result0 (LIST_CONJ [sub_bag_thm, thm1, thm2]) value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | encodeLib.sml | 1361 val result = PURE_REWRITE_RULE [AND_IMP_INTRO] value
|
| H A D | functionEncodeLib.sml | 693 let val result = match_disjunction thm term value
2183 val result = snd (EQ_IMP_RULE value
3328 val result value
3359 val result = DISCH_LIST_CONJ (mapfilter Option.valOf pres) value
[all...] |
| H A D | polytypicLib.sml | 1175 val result = check_standard_conv "SPLIT_FUNCTION_CONV" (term,snd (SFC pair_double ho_function_defs value
2408 else let val result = (cons s (cannon_type t) ; f t handle e => (tail s ; raise e)) in (tail s ; result) end value
2842 val result = conv term handle e => wrapException name e value
3311 val result = get_ind t value
3415 val result = complete_function name mk_term (C get_source_function_induction name) value
3430 val result = complete_function name mk_term (C (get_coding_function_induction target) name) value
3448 val result = complete_function name mk_term get_ind get_def get_func conv create_conv (dead_thm,dead_value) t (mthm,ethm) handle e => wrap e value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | FinalPolyML.sml | 2063 val result = value
[all...] |
| H A D | Foreign.sml | 761 val result value
2496 val result = resLoad rMem value
2526 val result = resLoad rMem value
2558 val result = resLoad rMem value
2594 val result = resLoad rMem value
2634 val result = resLoad rMem value
2681 val result = resLoad rMem value
2732 val result = resLoad rMem value
2788 val result = resLoad rMem value
2851 val result = resLoad rMem value
2920 val result = resLoad rMem value
2994 val result = resLoad rMem value
3073 val result = resLoad rMem value
3156 val result = resLoad rMem value
3243 val result = resLoad rMem value
3336 val result = resLoad rMem value
3391 val result = f arg1 value
3415 val result = f (arg1, arg2) value
3445 val result = f (arg1, arg2, arg3) value
3481 val result = f (arg1, arg2, arg3, arg4) value
3521 val result = f (arg1, arg2, arg3, arg4, arg5) value
3565 val result = f (arg1, arg2, arg3, arg4, arg5, arg6) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8.sml | 1162 val result = value
1240 val result = BitsN.fromNat(unsigned_sum,N) value
1350 val (result,nzc value
1363 val (result,nzcv) = AddWithCarry N (operand1,(operand2,carry_in)) value
1378 val (result,nzcv) = AddWithCarry N (operand1,(operand2,carry_in)) value
1394 val (result,nzcv) = AddWithCarry N (operand1,(operand2,carry_in)) value
1403 val result = value
1424 val result = value
1440 val result = value
1454 val result = ref (if opcode = MoveWideOp_K value
1464 val result = value
1533 val result = ref (BitsN.fromNat(0,N)) value
1551 val result = value
1566 val result = BitsN.fromBitstring(Bitstring.>>+(concat,lsb),N) value
1575 val result = value
1590 val result = value
1607 val result = value
1619 val result = value
1631 val result = value
1648 val result = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0.sml | 650 val result = value
1240 val result = ref 0 value
1294 ; let val result = BitsN.#>>(x,shift) in (result,BitsN.msb result) en value
1301 val result = value
1354 val result = BitsN.fromNat(unsigned_sum,N) value
1421 val (result,(carry,overflow)) = DataProcessingALU(opc,(rn,(imm32,C))) value
1446 val (result,_) = DataProcessingALU(opc,(rn,(imm32,C))) value
1502 val result = BitsN.*(R n,R m) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 1190 val result = BitsN.+(BitsN.+(x,y),BitsN.fromBool 64 carry) value
1204 val result = BitsN.-(x,BitsN.+(y,BitsN.fromBool 64 carry)) value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/ |
| H A D | dlmalloc.c | 4423 int result = 0; local
4828 int result = 0; local
4853 size_t result; local
4864 size_t result; local
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 2599 val result = DISCH (concl th1) (CHOOSE (���rep:'b->'a���,def) eth2) value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | xwindows.cpp | 1178 long result = GetRectRight(taskData, R) - GetRectLeft(taskData, R); local
1186 long result = GetRectBottom(taskData, R) - GetRectTop(taskData, R); local
6369 int result; local
9572 Handle result = 0; local
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 2063 val result = value
2890 val result = ref 0 value
2981 ; let val result = BitsN.#>>(x,shift) in (result,BitsN.msb result) en value
2988 val result = value
3094 val result = BitsN.fromNat(unsigned_sum,N) value
3924 val (result,(carry,overflow)) = value
3954 val (result,_) = DataProcessingALU(opc,(rn,(imm32,#C((!CPSR) : PSR)))) value
4056 val result = ref (BitsN.B(0x0,32)) value
4110 val result = BitsN.*(rn,rm) value
4132 val result = BitsN.+(BitsN.*(rn,rm),ra) value
4156 val result = value
4189 val result = value
4210 val result = value
4230 val result = IntInf.*(BitsN.toInt operand1,BitsN.toInt operand2) value
4240 val result = value
4259 val result = value
4273 val result = value
4297 val result = value
4324 val result = value
4339 val result = value
4343 val result = if round then IntInf.+(result,2147483648) else result value
4350 val result = value
4354 val result = if round then IntInf.+(result,2147483648) else result value
4769 val result = value
4806 val (result,sat) = value
4964 val result = ref (BitsN.toBitstring(R d)) value
6341 val (result,overflow) = SatQ 32 (i,(32,unsigned)) value
6358 val (result,overflow) = SatQ 32 (i,(32,unsigned)) value
[all...] |