Searched refs:gv (Results 1 - 25 of 39) sorted by relevance

12

/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/
H A DTreeBrowser.java21 GraphView gv; field in class:TreeBrowser
28 t = tn; gv = gr; font = f;
55 gv.collapseDir(v);
56 gv.relayout();
58 Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
59 gv.focusToVertex(l.getNumber());
60 vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
62 gv.getBrowser().viewFile(vx.getPath());
76 gv.collapseDir(v);
77 gv
[all...]
H A DGraphBrowser.java23 GraphView gv; field in class:GraphBrowser
120 gv.PS(fname,printable);
131 gv = new GraphView(new Graph(is, tn), this, font);
132 tb = new TreeBrowser(tn, gv, font);
133 gv.setTreeBrowser(tb);
136 gv.collapseDir(v);
140 scrollp1.add(gv);
197 gb.gv.PS(args[1], true);
199 gb.gv.PS(args[1], false);
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/
H A DTreeBrowser.java21 GraphView gv; field in class:TreeBrowser
28 t = tn; gv = gr; font = f;
55 gv.collapseDir(v);
56 gv.relayout();
58 Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
59 gv.focusToVertex(l.getNumber());
60 vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
62 gv.getBrowser().viewFile(vx.getPath());
76 gv.collapseDir(v);
77 gv
[all...]
H A DGraphBrowser.java23 GraphView gv; field in class:GraphBrowser
120 gv.PS(fname,printable);
131 gv = new GraphView(new Graph(is, tn), this, font);
132 tb = new TreeBrowser(tn, gv, font);
133 gv.setTreeBrowser(tb);
136 gv.collapseDir(v);
140 scrollp1.add(gv);
197 gb.gv.PS(args[1], true);
199 gb.gv.PS(args[1], false);
/seL4-l4v-master/HOL4/src/integer/
H A DjrhUtils.sml20 val gv = genvar (type_of x) value
22 EXT (GEN gv (* |- !gv. u gv =< (\x.t) gv *)
23 (TRANS (SPEC gv qth)
24 (SYM (BETA_CONV (mk_comb(tfun,gv)))))) end;
89 val gv = genvar (type_of l) value
90 val pat = subst[l |-> gv] w
92 ([(asl,a), (asl,subst[gv |
[all...]
H A DCSimp.sml70 val gv = genvar int_ty value
75 val eq1 = MP (INST [cvar |-> varpart, xvar |-> numpart, yvar |-> gv]
78 yvar |-> gv]
91 | POSITIVE => (K (INST [gv |-> rand (rand t)] eq1) THENC
93 | NEGATED => (K (INST [gv |-> rand (rand t)] eq2) THENC
103 yvar |-> gv] le_context_rwt1) ltthm
105 yvar |-> gv] le_context_rwt2) ltthm)
107 yvar |-> gv] le_context_rwt3) ltthm
109 yvar |-> gv] le_context_rwt4) ltthm)
124 (INST [gv |
[all...]
H A DIntDP_Munge.sml179 val gv = genvar int_ty value
181 mk_forall(gv, subst [bv |-> gv] t)
201 val gv = genvar int_ty value
202 val tm1 = subst [inj_n |-> gv] tm
204 GSYM (BETA_CONV (mk_comb(mk_abs(gv,tm1), inj_n)))
400 val gv = genvar numSyntax.num value
401 val newterm = mk_forall (gv, Term.subst [subtm |-> gv] tm)
429 val gv value
445 val gv = genvar int_ty value
[all...]
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DsexpScript.sml213 (* (gv binary-+ (x y) x)) *)
214 (* (gv binary-+ (x y) *)
242 (* (gv binary-* (x y) 0)) *)
243 (* (gv binary-* (x y) 0)))) *)
256 (* (gv < (x y) *)
290 (* (gv unary-- (x) 0)))) *)
305 (* (gv unary-/ (x) 0)))) *)
342 (* (t (gv car (x) nil)))) *)
362 (* (t (gv cdr (x) nil)))) *)
379 (* (gv realpar
[all...]
H A Dmake_sexp.ml187 (* (gv binary-+ (x y) x)) *)
188 (* (gv binary-+ (x y) *)
216 (* (gv binary-* (x y) 0)) *)
217 (* (gv binary-* (x y) 0)))) *)
230 (* (gv < (x y) *)
264 (* (gv unary-- (x) 0)))) *)
279 (* (gv unary-/ (x) 0)))) *)
316 (* (t (gv car (x) nil)))) *)
336 (* (t (gv cdr (x) nil)))) *)
353 (* (gv realpar
[all...]
/seL4-l4v-master/HOL4/src/1/
H A DFullUnify.sml146 val gv = genvar (type_of bv1) value
148 recurse (gv::bvs)
149 (subst [bv1 |-> gv] bod1, subst [bv2 |-> gv] bod2)
H A DHo_Rewrite.sml234 val gv = genvar(type_of stm) value
235 val abs = mk_abs(gv,subst[stm |-> gv] tm)
H A DPmatch.sml96 fun fresh_constr ty_match (colty:hol_type) gv c =
101 val gvars = map (inst ty_theta o gv) L
147 | partitionl gv ty_match
173 | partition gv ty_match
175 let val fresh = fresh_constr ty_match colty gv
269 fun mk_switch_tm gv v base literals =
272 val v' = last literals handle _ => gv lty
273 fun mk_arg lit = if is_var lit then gv (lty --> rty) else gv rty
H A DMutual.sml259 let val gv = genvar(type_of v) value
262 in TRANS th (GEN_ALPHA_CONV gv (rhs(concl th)))
H A DDrule.sml243 val gv = genvar (type_of Bvar) value
245 EXT (GEN gv (TRANS (TRANS (BETA_CONV (mk_comb (ufun, gv))) (SPEC gv qth))
246 (SYM (BETA_CONV (mk_comb (vfun, gv))))))
2735 (%gv /\ ?x. Q x) = (?x. %gv /\ Q x)
2739 (%gv /\ ?P. Q P) = (?P. %gv /\ Q P)
2742 %gv [
[all...]
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A DsexpScript.sml213 (* (gv binary-+ (x y) x)) *)
214 (* (gv binary-+ (x y) *)
242 (* (gv binary-* (x y) 0)) *)
243 (* (gv binary-* (x y) 0)))) *)
256 (* (gv < (x y) *)
290 (* (gv unary-- (x) 0)))) *)
305 (* (gv unary-/ (x) 0)))) *)
342 (* (t (gv car (x) nil)))) *)
362 (* (t (gv cdr (x) nil)))) *)
379 (* (gv realpar
[all...]
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A DsexpScript.sml213 (* (gv binary-+ (x y) x)) *)
214 (* (gv binary-+ (x y) *)
242 (* (gv binary-* (x y) 0)) *)
243 (* (gv binary-* (x y) 0)))) *)
256 (* (gv < (x y) *)
290 (* (gv unary-- (x) 0)))) *)
305 (* (gv unary-/ (x) 0)))) *)
342 (* (t (gv car (x) nil)))) *)
362 (* (t (gv cdr (x) nil)))) *)
379 (* (gv realpar
[all...]
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A DholfootParser.sml801 fun holfoot_p_statement2absyn funL resL gv vs (Pstm_assign (v, expr)) =
809 | holfoot_p_statement2absyn funL resL gv vs (Pstm_fldlookup (v, expr, tag)) =
818 | holfoot_p_statement2absyn funL resL gv vs (Pstm_fldassign (expr1, tag, expr2)) =
827 | holfoot_p_statement2absyn funL resL gv vs (Pstm_new (v, expr, tl)) =
837 | holfoot_p_statement2absyn funL resL gv vs (Pstm_dispose (expr1, expr2)) =
845 | holfoot_p_statement2absyn funL resL gv vs Pstm_diverge =
847 | holfoot_p_statement2absyn funL resL gv vs Pstm_fail =
849 | holfoot_p_statement2absyn funL resL gv vs (Pstm_block stmL) =
851 val l0 = map (holfoot_p_statement2absyn funL resL gv vs) stmL;
858 | holfoot_p_statement2absyn funL resL gv v
[all...]
/seL4-l4v-master/isabelle/src/Tools/Graphview/
H A Dmutator.scala123 (gv, key) => {
136 add_edges(gv, from.imm_preds(key), false),
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/
H A Dmutator.scala123 (gv, key) => {
136 add_edges(gv, from.imm_preds(key), false),
/seL4-l4v-master/HOL4/src/pred_set/src/
H A DPGspec.sml54 val gv = genvar ty2 value
55 in SUBST [gv |-> MK_PAIR (tl vs) snd] (mk_eq(v,mk_pair(fst,gv))) inst
H A DPFset_conv.sml97 val gv = genvar bool value
99 val F_OR = el 3 (CONJUNCTS (SPEC gv OR_CLAUSES))
100 val OR_T = el 2 (CONJUNCTS (SPEC gv OR_CLAUSES))
116 val thm3 = INST[gv |-> rand(concl rthm)] F_OR
126 val thm3 = TRANS thm2 (INST [gv |-> eqn] OR_T)
/seL4-l4v-master/HOL4/src/monad/more_monads/
H A Dstate_transformerScript.sml81 f = BIND g (\gv. if gv then IGNORE_BIND b f else UNIT ())``,
/seL4-l4v-master/HOL4/src/refute/
H A DCanon.sml65 val gv = genvar(type_of stm) value
66 val th1 = ASSUME(mk_eq(gv,stm))
646 val gv = genvar(type_of t) value
647 val abs = mk_abs(gv,subst[t |-> gv] tm)
/seL4-l4v-master/HOL4/examples/lambda/other-models/
H A DncScript.sml735 (Q.prove(`?gv:string.
736 ~(gv IN FV ^u UNION FV (u1:'a nc) UNION {x;x1})`,
747 THEN X_CHOOSE_THEN (Term`gv:string`) STRIP_ASSUME_TAC (GSYM lemma)
748 THEN let val ac1 = UNDISCH(Q.SPECL [`gv`, `u`] SIMPLE_ALPHA)
749 val ac2 = UNDISCH(Q.SPECL [`gv`,`u1`] SIMPLE_ALPHA)
/seL4-l4v-master/HOL4/src/tfl/src/
H A DInduction.sml72 fun ipartition gv (constructors,rows) =
95 new_formals = map gv col_types,
193 val gv = (wfrecUtils.vary FV) value
194 val divide:divide_ty = ipartition gv

Completed in 269 milliseconds

12