/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_symbolsScript.sml | 1518 ?fail g2 f2 toosmall. 1522 (r7,n2w (n+LENGTH xs) << 3 !! 3w,1w,dg,g2,df,f2)) /\ 1525 (ref_static (r7 - 0xD8w) [sa2+n2w (LENGTH s + 1);sa3] * q) (fun2set (f2,df)) /\ 2265 \\ `w2w (f2 (sp - 236w)) << 32 !! w2w (f2 (sp - 240w)) = (n2w e):word64` by 2267 \\ Q.PAT_X_ASSUM `xxx (fun2set (f2,df))` MP_TAC 2327 \\ Q.PAT_X_ASSUM `xxx (fun2set (f2,df))` MP_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/mlton/ |
H A D | evalML.sml | 444 val (nzcv2, (i2, (f2, m2))) = armML.DECODE_PSR cpsr2
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ProjectionScript.sml | 1883 (F_CLOCK_FREE (F_AND(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2) 1891 (F_CLOCK_FREE (F_UNTIL(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2)
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | ellipticScript.sml | 1392 ``!f1 f2 :: Field. !f :: FieldHom f1 f2. !e :: Curve.
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sml | 420 fun try_alt f1 f2 strm = 422 of NONE => f2 strm
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Term.sml | 942 | (App(f1, x1), App(f2, x2)) => 943 RM (TMP (f1, f2) :: TMP (x1, x2) :: rest) theta0
|
/seL4-l4v-10.1.1/HOL4/src/meson/test/ |
H A D | selftest.sml | 699 (!X. program_decides(X) \/ program(f2(X))) /\ 700 (!X. decides(X,f2(X),f1(X)) ==> program_decides(X)) /\ 2940 (!X. ordered_pair_predicate(X) ==> little_set(f2(X))) /\ 2942 (!X. ordered_pair_predicate(X) ==> equal(X,ordered_pair(f2(X),f3(X)))) /\ 3073 (!A2 B2. equal(A2,B2) ==> equal(f2(A2),f2(B2))) /\ 3285 (!U Vf. element_of_set(U,intersection_of_members(Vf)) \/ element_of_collection(f2(Vf,U),Vf)) /\ 3286 (!Vf U. element_of_set(U,f2(Vf,U)) ==> element_of_set(U,intersection_of_members(Vf))) /\
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | translateScript.sml | 619 ``pair f1 f2 o (g1 ## g2) = pair (f1 o g1) (f2 o g2)``,
|
H A D | fmap_encodeScript.sml | 946 val fix_fmap_def = Define `fix_fmap f1 f2 = list (pair I I) o 947 QSORT3 ($<= LEX (K (K T))) o M2L o L2M o sexp_to_list (sexp_to_pair I I) o fix_list (fix_pair f1 f2)`;
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | CommonDialog.sml | 1357 val f2 = case logFont of SOME _ => CF_INITTOLOGFONTSTRUCT | _ => 0w0 value 1359 val flags = List.foldl LargeWord.orb 0w0 [ChooseFontFlags.toWord flags, f1, f2, f3]
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | probScript.sml | 4054 ``!p f1 f2 g1 g2. 4055 f1 IN indep_fn /\ f2 IN indep_fn /\ 4057 (!m. prob bern ($= m o FST o f1) = prob bern ($= m o FST o f2)) /\ 4059 (prob bern (p o FST o BIND f1 g1) = prob bern (p o FST o BIND f2 g2))``, 4061 >> Know `countable (range (FST o f1) UNION range (FST o f2))` 4069 >> MP_TAC (Q.SPECL [`p`, `f2`, `g2`, `f`] PROB_BERN_BIND_COUNTABLE)
|
/seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
H A D | lhs_pars.py | 2293 f2 = open('caseconvs-useful', 'w') 2313 render_caseconv(cases, to_case, f2) 2320 f2.close()
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ILTheory.sml | 1383 bool)), V"f2" ((T"MREG" "IL" [] --> (T"MEXP" "IL" [] --> alpha))), 1797 V"f2" 3119 V"f2'" ((T"MREG" "IL" [] --> (T"MEXP" "IL" [] --> alpha))), 3210 V"f2'" 3244 V"f2"
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/ |
H A D | decompilerLib.sml | 331 val f2 = CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV) value 333 val (th1,th2) = if is_neg t1 then (f2 th1,f1 th2) else (f1 th1, f2 th2)
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/doc/ |
H A D | ds.tex | 498 `sf_bin_tree (f1, f2) e = sf_tree [f1;f2] dse_nil e`;
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/ |
H A D | m0_stepLib.sml | 1345 val f2 = lsub s2 value 1346 fun loop i = i >= n orelse f1 i = f2 i andalso loop (i + 1)
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | PairRules.sml | 2009 let val (f1,f2) = dest_pair f 2032 (P_PSKOLEM_CONV f2))))
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 1247 val (ys,f2,df2) = dest_fun2set tm2 1268 fun term_full (tm1,tm2) = (mk_comb(tm1,mk_fun2set(f1,df1)),mk_comb(tm2,mk_fun2set(f2,df2)))
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | lzPairRules.sml | 2030 let val (f1,f2) = dest_pair f 2053 (P_PSKOLEM_CONV f2))))
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | config.guess | 1020 case `grep '^cpu[^a-z]*:' /proc/cpuinfo 2>/dev/null | cut -d' ' -f2` in
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | config.guess | 1020 case `grep '^cpu[^a-z]*:' /proc/cpuinfo 2>/dev/null | cut -d' ' -f2` in
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceFunctor.sml | 3780 fun f2 x = if !verbose_level = 0 andalso !verbose_level_try = 0 then f1 x else function 3788 in f2 end 3794 fun f2 p context dir t = function 3797 f2
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | concrwaa2gbaScript.sml | 74 >> `(���f1 f2. f = U f1 f2)` by (Cases_on `f` >> fs[is_until_def]) >> simp[] 79 >> `���f1 f2. x.frml = U f1 f2` by metis_tac[] 3961 (��(eL1,f1) (eL2,f2). eL1.edge_grp = eL2.edge_grp)
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Defn.sml | 1479 ``(f1 x = f2 (x-1) + f5 (x-1)) /\ 1480 (f2 x = f3 (x-1) + f4 (x-1)) /\
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | GraphLangScript.sml | 1400 \\ MATCH_MP_TAC (METIS_PROVE [] ``(f1 = f2) /\ (x1 = x2) ==> (f1 x1 = f2 x2)``)
|