/seL4-l4v-master/HOL4/src/new-datatype/ |
H A D | NDatatype.sml | 244 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 D | core_decompilerLib.sml | 589 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 D | Help.sml | 214 {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 D | makebase.sml | 30 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 D | HOLPage.sml | 61 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 D | Subst.sml | 94 fun comp mk_cl = function
|
H A D | Term.sml | 78 | 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 D | Portable.sml | 294 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 D | test_wordppScript.sml | 116 val _ = set_trace "word pp as 2's comp" 1;
|
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/ |
H A D | LambekScript.sml | 76 (!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 D | PGspec.sml | 79 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 D | ens_catScript.sml | 112 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 D | functorScript.sml | 941 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 D | nat_transScript.sml | 258 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 D | zfset_catScript.sml | 243 comp := ��f g. (g |o| f).map |>`;
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | wordspp.sml | 15 val _ = Feedback.register_btrace ("word pp as 2's comp", int_word_pp)
|
/seL4-l4v-master/graph-refine/ |
H A D | logic.py | 1343 comp = [] 1349 comp.append (x) 1350 comps.append ((v2, comp)) 1448 if not [comp for comp in comps if comp[1]]:
|
H A D | problem.py | 757 return [comp for comp in comps if comp[1]]
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | decompTools.sml | 169 (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 D | finite_mapScript.sml | 1068 ?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 D | switching_lemmaScript.sml | 497 `` ���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 D | permLib.sml | 531 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 D | substScript.sml | 770 `!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 D | ml.tex | 11 \texttt{comp.lang.ml}\footnote{\url{http://www.faqs.org/faqs/meta-lang-faq/}}.
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | String.sml | 1393 fun comp' i = 1403 General.EQUAL => comp' (i+0w1) 1407 comp' 0w0
|