/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | patricia_castsScript.sml | 192 \\ sg `LENGTH l1 = LENGTH l2`
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | pydot.py | 1631 for sg in self.obj_dict['subgraphs'].itervalues(): 1632 sgraph_obj_dicts.extend(sg)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | progScript.sml | 62 INIT_TAC \\ sg `CODE_POOL instr {} = emp`
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Prim_rec.sml | 595 | GOALS A [t] tm = let val (sg,pf) = t (A,tm) in ([sg],[pf]) end value 599 val (sg,pf) = h (A,conj1) value 600 in (sg::sgs, pf::pfs)
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_equalScript.sml | 18 fun SUBGOAL q = REVERSE (sg q)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | arm_cheney_gcScript.sml | 215 \\ sg c \\ ASM_REWRITE_TAC [APPLY_UPDATE_THM] 404 (sg `{ax;ay} SUBSET0 D1(CUT(i,j)m)` THENL [
|
H A D | arm_cheney_allocScript.sml | 332 \\ sg `ch_mem (i,e,rs,l,u,m) (a,x,xs1)` THENL [
|
H A D | improved_gcScript.sml | 10 fun SUBGOAL q = REVERSE (sg q) 683 \\ sg `ADDR_SET [H_DATA a] = {}` \\ ASM_SIMP_TAC std_ss [full_heap_REFL]
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_equalScript.sml | 226 \\ REVERSE (sg `MAX_ADDRESSES (r7 - 8w) (q::MAP FST t) SUBSET e`) THENL [ 270 \\ sg `MAX_ADDRESSES (r7 + 8w) (x1::x2::MAP FST ys) SUBSET e`
|
/seL4-l4v-10.1.1/HOL4/Manual/Interaction/ |
H A D | HOL-interaction.tex | 469 We can start such a subproof by typing {\tt\small sg \sq h n = g n\sq}.% 484 {\tt\small sg \sq h n = g n\sq}. If the sub-goal requires
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | integralScript.sml | 1715 ABBREV_TAC``sg = rsum(d,p) (g ((N1:num) + N2))`` THEN 1718 EXISTS_TAC``abs(sf - sg) + abs(sg - i((N1:num)+ N2))`` THEN 1721 EXISTS_TAC``abs((sf - sg) + (sg - i((N1:num) + N2)))`` THEN
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_opsScript.sml | 174 \\ sg `CODE_POOL X86_INSTR ((a,xs ++ ys,w) INSERT c) =
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/garbage-collector/ |
H A D | stop_and_copyScript.sml | 10 fun SUBGOAL q = REVERSE (sg q) 701 \\ sg `ADDR_SET [H_DATA a] = {}` \\ ASM_SIMP_TAC std_ss [full_heap_REFL]
|
H A D | lisp_consScript.sml | 15 fun SUBGOAL q = REVERSE (sg q)
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | for_compileScript.sml | 857 \\ REVERSE (sg `!c. ?s. sem_a (a_state (phase3 0 0 t) c) = (Rtimeout,s)`)
|
H A D | for_nd_compileScript.sml | 1006 \\ sg `!c. FILTER ISL (SND (sem_t (init_st c (K F) input) t)).io_trace =
|
/seL4-l4v-10.1.1/HOL4/src/basicProof/ |
H A D | BasicProvers.sml | 393 val sg = subgoal value
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesScript.sml | 830 sg `(i'=0) \/ (?i''. (i' = SUC i''))` THENL [
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | generalHelpersScript.sml | 1304 sg `!L1 L2 x. MEM x (MAP FST L2) ==>
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_proofpScript.sml | 733 \\ REVERSE (sg `?t. (h = a2sexp t) /\ appeal_syntax_ok t`) 837 (sg `(MAP t2sexp l = MAP t2sexp l') = (l = l')` \\ FS [] 849 \\ sg `(MAP t2sexp l0 = MAP t2sexp l0') = (l0 = l0')` 1674 \\ sg `(logic_flag_callmap (Sym "TERM") (Sym name) (t2sexp h) = 3031 \\ sg `lookup_safe (Sym fname) ftbl = list2sexp [Sym fname]` 3287 \\ sg `term_ok ctxt (term2t (sexp3term h)) /\ 3308 \\ sg `EVERY (term_ok ctxt) (MAP (term2t o sexp3term) t)`
|
H A D | milawa_execScript.sml | 1272 \\ STRIP_TAC \\ sg `F` \\ FULL_SIMP_TAC std_ss [] 1960 \\ sg `MAP (\v. (v,mConst (if h' = v then h else FunVarBind params t v)))
|
H A D | milawa_logicScript.sml | 1078 \\ sg `MAP (EvalTerm (a,ctxt)) args = MAP (EvalTerm (b,ctxt)) args` 1281 (sg `MAP (\a''. EvalTerm (a,ctxt |+ (fname,params,body,sem)) a'') ys =
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootScript.sml | 1141 sg `VAR_RES_IS_STACK_IMPRECISE P1 /\ VAR_RES_IS_STACK_IMPRECISE P2`) THEN1 ( 4824 sg `(e3 (FST s) = SOME (s1''' ' c1 tl)) /\ 5321 sg `!s1 s2 n' data. 7956 sg `(!s. (s IN P1 = ?e'. s IN P1' e')) /\ 8345 Tactical.REVERSE (sg `~(v IN FDOM (FST s0))`) THEN ASM_SIMP_TAC std_ss [] THEN 8593 sg `(t IN FDOM L') /\ (L' ' t = var_res_exp_const (EL (e - ds) tdata))`) THEN1 (
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | sexp.sml | 2257 | dest_acl2def (encap(sg,tm)) = ("ENCAPSULATE", concat_with_spaces sg);
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexp.sml | 2181 | dest_acl2def (encap(sg,tm)) = ("ENCAPSULATE", concat_with_spaces sg);
|