Searched refs:comp (Results 26 - 50 of 55) sorted by relevance

123

/seL4-l4v-master/HOL4/src/new-datatype/
H A DNDatatype.sml244 val comp = compose dict self pty value
245 in {inj_pair = gen_inj_pair_thm (#inj_pair comp) maps rets,
246 ret_map = gen_ret_map_thm (#ret_map comp) maps' rets,
247 all_tm = list_mk_abs(alls, #all_tm comp),
249 all_map = gen_ret_map_thm (#all_map comp) maps' alls,
250 all_T = #all_T comp,
251 all_mono = gen_all_mono_thm (#all_mono comp) rtcs
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/
H A Dcore_decompilerLib.sml589 fun comp (End i) = exit_th function
590 | comp (Repeat i) = enter_th
591 | comp (Cons (th, t)) = compose th (comp t)
592 | comp (Merge (tm, t1, t2)) = merge tm (comp t1) (comp t2)
593 | comp (ConsMerge (tm, th1, th2, t)) =
595 val res = comp t
601 (comp
[all...]
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DHelp.sml214 {comp = Str, file, ...} =>
216 | {comp = Term _, file, line} =>
218 | {comp, file, line} =>
254 fun render (entry as {comp, file, ...}) =
255 case comp of
/seL4-l4v-master/HOL4/help/src-sml/
H A Dmakebase.sml30 fun isTheory {comp,file=path,line} =
38 fun isSigId {comp=Database.Term(_,SOME"HOL"),file,line} = false
109 fun kindCompare (e1 as {comp=c1, ...}, e2 as {comp=c2, ...}) =
154 {comp=Database.Term(Symbolic.tosymb content, SOME"HOL"),
H A DHOLPage.sml61 fun class_of drop {comp=Str, file, line} =
72 fun misc_struct_of {comp=Str, file, line} =
/seL4-l4v-master/HOL4/src/0/
H A DSubst.sml94 fun comp mk_cl = function
H A DTerm.sml78 | mk_clos (s,Clos(Env,Body)) = Clos(Subst.comp mk_clos (s,Env), Body)
958 local val subs_comp = Subst.comp mk_clos
/seL4-l4v-master/HOL4/src/portableML/
H A DPortable.sml294 fun comp ([], []) = EQUAL function
295 | comp ([], _) = LESS
296 | comp (_, []) = GREATER
297 | comp (h1 :: t1, h2 :: t2) =
298 case cfn (h1, h2) of EQUAL => comp (t1, t2) | x => x
300 comp
/seL4-l4v-master/HOL4/src/n-bit/interactive_tests/
H A Dtest_wordppScript.sml116 val _ = set_trace "word pp as 2's comp" 1;
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/
H A DLambekScript.sml76 (!X A B C. arrow X A B /\ arrow X B C ==> arrow X A C) /\ (* comp *)
79 val [one, beta, beta', gamma, gamma', comp, arrow_plus] =
81 (combine (["one", "beta", "beta'", "gamma", "gamma'", "comp", "arrow_plus"],
100 REWRITE_TAC [transitive_def, comp]);
164 >> MATCH_MP_TAC comp
175 >> MATCH_MP_TAC comp
185 >> MATCH_MP_TAC comp
195 >> MATCH_MP_TAC comp
206 >> MATCH_MP_TAC comp
219 >> MATCH_MP_TAC comp
[all...]
/seL4-l4v-master/HOL4/src/pred_set/src/
H A DPGspec.sml79 val comp = pairSyntax.strip_pair (rand(concl tupeq)) value
80 val thm1 = Lib.itlist2 EX vs comp asm1
/seL4-l4v-master/HOL4/examples/category/
H A Dens_catScript.sml112 comp := ��f g. (g o f).map |>`;
162 `���U f g. f ���> g -:(ens_cat U) ��� ((ens_cat U).comp f g = ComposeFun(f.dom,g.dom) g.map f.map)`,
H A DfunctorScript.sml941 comp := (��x y. ((FST y.map) o (FST x.map) -:t.dom,
1020 `(compose (pre_comma_cat t s).comp f g ���> h -:pre_comma_cat t s)` by (
1031 `(f ���> compose (pre_comma_cat t s).comp g h -:pre_comma_cat t s)` by (
1156 comp := ��f g. (g ��� f).map |>`;
H A Dnat_transScript.sml258 comp := (��n m. (nt_comp m n).map) |>`;
277 `���c1 c2 n m. (pre_functor_cat c1 c2).comp n m = (nt_comp m n).map`,
366 `���c1 c2 n m. n ������> m ��� (ntdom m = c1) ��� (ntcod m = c2) ��� ([c1���c2].comp n m = (nt_comp m n).map)`,
H A Dzfset_catScript.sml243 comp := ��f g. (g |o| f).map |>`;
/seL4-l4v-master/HOL4/src/n-bit/
H A Dwordspp.sml15 val _ = Feedback.register_btrace ("word pp as 2's comp", int_word_pp)
/seL4-l4v-master/graph-refine/
H A Dlogic.py1343 comp = []
1349 comp.append (x)
1350 comps.append ((v2, comp))
1448 if not [comp for comp in comps if comp[1]]:
H A Dproblem.py757 return [comp for comp in comps if comp[1]]
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DdecompTools.sml169 (get_prop_type (fst (dest_forall (concl gpsdth)))))))))(* lifted type's state's snd comp *)
219 val ns_ty = type_of s2 (* lifted type's state's snd comp *)
/seL4-l4v-master/HOL4/src/finite_maps/
H A Dfinite_mapScript.sml1068 ?comp. (FDOM comp = FDOM g INTER { x | FAPPLY g x IN FDOM f })
1069 /\ (!x. x IN FDOM comp ==>
1070 (FAPPLY comp x = (FAPPLY f (FAPPLY g x))))`,
1075 Q.EXISTS_TAC `FUPDATE comp (x, FAPPLY f y)` THEN
1078 Q.EXISTS_TAC `comp` THEN
1105 ?comp. (FDOM comp = FDOM g)
1106 /\ (!x. x IN FDOM comp ==> (FAPPLY comp
[all...]
/seL4-l4v-master/HOL4/examples/ARM_security_properties/
H A Dswitching_lemmaScript.sml497 `` ���g s1 s2 comp scr u.
498 ((comp = (condT (F) (write_scr <|proc := 0|> (scr with NS := F))
500 (comp = (condT (F) (write_scr <|proc := 0|> (scr with NS := F))
509 ( comp s1 = ValueState a s1') ���
510 ( comp s2 = ValueState a s2') ���
519 ���e. (comp s1 = Error e) ��� (comp s2 = Error e)``,
/seL4-l4v-master/HOL4/src/sort/
H A DpermLib.sml531 val comp = pair_compare (list_compare Term.compare, list_compare Term.compare); value
538 (comp ((xs1,ls1), (xs2,ls2)) = LESS))
/seL4-l4v-master/HOL4/examples/unification/triangular/first-order/
H A DsubstScript.sml770 `!s2 s1.?comp.!x.(subst_APPLY comp x = (subst_APPLY s2 (subst_APPLY s1 x)))`,
774 Q.EXISTS_TAC `comp |+ (x,s2 ��� y)` >>
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dml.tex11 \texttt{comp.lang.ml}\footnote{\url{http://www.faqs.org/faqs/meta-lang-faq/}}.
/seL4-l4v-master/HOL4/polyml/basis/
H A DString.sml1393 fun comp' i =
1403 General.EQUAL => comp' (i+0w1)
1407 comp' 0w0

Completed in 374 milliseconds

123