/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeBrowser.java | 21 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 D | GraphBrowser.java | 23 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 D | TreeBrowser.java | 21 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 D | GraphBrowser.java | 23 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 D | jrhUtils.sml | 20 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 D | CSimp.sml | 70 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 D | IntDP_Munge.sml | 179 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 D | sexpScript.sml | 213 (* (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 D | make_sexp.ml | 187 (* (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 D | FullUnify.sml | 146 val gv = genvar (type_of bv1) value 148 recurse (gv::bvs) 149 (subst [bv1 |-> gv] bod1, subst [bv2 |-> gv] bod2)
|
H A D | Ho_Rewrite.sml | 234 val gv = genvar(type_of stm) value 235 val abs = mk_abs(gv,subst[stm |-> gv] tm)
|
H A D | Pmatch.sml | 96 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 D | Mutual.sml | 259 let val gv = genvar(type_of v) value 262 in TRANS th (GEN_ALPHA_CONV gv (rhs(concl th)))
|
H A D | Drule.sml | 243 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 D | sexpScript.sml | 213 (* (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 D | sexpScript.sml | 213 (* (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 D | holfootParser.sml | 801 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 D | mutator.scala | 123 (gv, key) => { 136 add_edges(gv, from.imm_preds(key), false),
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/ |
H A D | mutator.scala | 123 (gv, key) => { 136 add_edges(gv, from.imm_preds(key), false),
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | PGspec.sml | 54 val gv = genvar ty2 value 55 in SUBST [gv |-> MK_PAIR (tl vs) snd] (mk_eq(v,mk_pair(fst,gv))) inst
|
H A D | PFset_conv.sml | 97 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 D | state_transformerScript.sml | 81 f = BIND g (\gv. if gv then IGNORE_BIND b f else UNIT ())``,
|
/seL4-l4v-master/HOL4/src/refute/ |
H A D | Canon.sml | 65 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 D | ncScript.sml | 735 (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 D | Induction.sml | 72 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
|