/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | closure.sml | 13 let g2 x = x + 2 in 14 (twice(g1,z),twice(g2,z))`; 29 val g2'_def = Define ` 30 g2' x = x + 2`; 36 G2 -> g2' i 45 let g2:clos = G2 in 46 (twice1(g1,z),twice1(g2,z))`; 57 twice_def, dispatch_def,g1'_def, g2'_def]
|
H A D | gr_t.sml | 207 val (r,g2) = gfoldn (f c) g1 208 in (d (l,r),g2) end 212 val (y,g2) = gfoldn l g1 213 in (b (x,y),g2) end 283 val (r,g2) = gfoldn (f c) g1 284 in (d (l,r),g2) end 288 val (y,g2) = gfoldn l g1 289 in (b (x,y),g2) end
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | closure.sml | 13 let g2 x = x + 2 in 14 (twice(g1,z),twice(g2,z))`; 29 val g2'_def = Define ` 30 g2' x = x + 2`; 36 G2 -> g2' i 45 let g2:clos = G2 in 46 (twice1(g1,z),twice1(g2,z))`; 57 RW_TAC std_ss [g1'_def, g2'_def]
|
H A D | gr_t.sml | 207 val (r,g2) = gfoldn (f c) g1 208 in (d (l,r),g2) end 212 val (y,g2) = gfoldn l g1 213 in (b (x,y),g2) end 283 val (r,g2) = gfoldn (f c) g1 284 in (d (l,r),g2) end 288 val (y,g2) = gfoldn l g1 289 in (b (x,y),g2) end
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | closure.sml | 13 let g2 x = x + 2 in 14 (twice(g1,z),twice(g2,z))`; 29 val g2'_def = Define ` 30 g2' x = x + 2`; 36 G2 -> g2' i 45 let g2:clos = G2 in 46 (twice1(g1,z),twice1(g2,z))`; 57 RW_TAC std_ss [g1'_def, g2'_def]
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | multidim_arrays.c | 31 int g2(struct s* sptr, int i, int j) function 43 return g2(&global2, i, j);
|
H A D | jiraver439.c | 26 unsigned g2(void) function
|
H A D | automatic_modifies.c | 28 void g2(int j) function
|
/seL4-l4v-10.1.1/HOL4/examples/miller/groups/ |
H A D | abelian_groupScript.sml | 138 !g1 g2 :: gset G. ?h :: gset G. gord G h = lcm (gord G g1) (gord G g2)``, 141 `!g. !g1 g2 :: gset G. 142 (gcd (gord G g1) (gord G g2) = g) ==> 143 ?h :: gset G. gord G h = lcm (gord G g1) (gord G g2)` 145 ++ Q.PAT_X_ASSUM `!g. P g` (MP_TAC o Q.SPEC `gcd (gord G g1) (gord G g2)`) 151 ++ Q_RESQ_EXISTS_TAC `gop G g1 g2` 155 ++ MP_TAC (Q.SPECL [`gord G g1`, `gord G g2`] FACTOR_GCD) 161 ++ Know `p * gord G (gpow G g2 p) = gord G g2` [all...] |
H A D | groupScript.sml | 260 ``!G H g1 g2 h1 h2. 261 gop (prod_group G H) (g1, h1) (g2, h2) = (gop G g1 g2, gop H h1 h2)``, 504 ``!G :: group. !H :: subgroup G. !g1 g2 :: gset G. 505 (lcoset G g1 H = lcoset G g2 H) 506 \/ DISJOINT (lcoset G g1 H) (lcoset G g2 H)``, 510 /\ g IN lcoset G g2 H`) 517 ++ Suff `!v. v IN lcoset G g1 H = v IN lcoset G g2 H` 522 ++ Q.SPEC_TAC (`g2`, `g2`) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/generic_finite_graphs/ |
H A D | gfgScript.sml | 79 `wfg g ��� (addEdge i (e,s) g = SOME g2) ==> wfg g2`, 96 `(addEdge i (e,s) g) = SOME g2 ==> (g.nodeInfo = g2.nodeInfo)`, 102 `wfg g ��� (updateNode id n g = SOME g2) ==> wfg g2`, 111 `updateNode id n g = SOME g2 112 ==> (g.followers = g2.followers) 113 ��� (g.preds = g2.preds)`, 120 `updateNode id n g = SOME g2 [all...] |
/seL4-l4v-10.1.1/HOL4/src/tfl/examples/ |
H A D | ctlScript.sml | 144 /\ (ACTLSTAR_PATH (g1 \/ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2) 145 /\ (ACTLSTAR_PATH (g1 /\ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2) 149 /\ (ACTLSTAR_PATH (g1 U g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2) 150 /\ (ACTLSTAR_PATH (g1 R g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)`; 259 /\ (PATHSAT (M,PI) (g1 \/ g2) = PATHSAT (M,PI) g1 \/ PATHSAT (M,PI) g2) [all...] |
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/ |
H A D | pattern_matchingScript.sml | 61 val _ = def "g2" 62 `(g2 ([]:'a list, CONS a (CONS b x)) = 1) /\ 63 (g2 (CONS a (CONS b x), y) = 2) /\ 64 (g2 (z, CONS a y) = 3)`;
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | NDDB.sml | 109 prove(``!f1 g1 f2 g2. 110 ((sum_retrieve g1 g2)o h) o ((sum_map f1 f2)o h) = 111 ((sum_retrieve (g1 o f1) (g2 o f2)) o h)`` 119 val sum_inj_pair_thm = prove(``!f1 g1 f2 g2. 121 (inj_pair f2 g2) ==> 122 (inj_pair (sum_map f1 f2) (sum_retrieve g1 g2))``, 130 val sum_retrieve_map_thm = prove(``!f1 g1 f2 g2. 131 (sum_retrieve g1 g2) o (sum_map f1 f2) = 132 (sum_retrieve (g1 o f1) (g2 o f2)) 178 val prod_inj_pair_thm = prove(``!f1 g1 f2 g2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | encap1.lisp | 56 ; Definition. g2 = some g2 . (integerp (mv-nth 0 (g2 x))) 57 ; |- forall x . |= (integerp (mv-nth 0 (g2 x))) 59 ((g2 (x) (mv t t))) 60 (local (defun g2 (x) 63 (defthm integerp-first-g2 64 (integerp (mv-nth 0 (g2 x)))))
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/encap/ |
H A D | example.lisp | 54 ; Definition. g2 = some g2 . (integerp (mv-nth 0 (g2 x))) 55 ; |- forall x . |= (integerp (mv-nth 0 (g2 x))) 57 ((g2 (x) (mv t t))) 58 (local (defun g2 (x) 61 (defthm integerp-first-g2 62 (integerp (mv-nth 0 (g2 x)))))
|
/seL4-l4v-10.1.1/l4v/proof/infoflow/tools/ |
H A D | authority2infoflow-CaML.ml | 268 let g2=[("T",ASyncSend,"AEP1");("T",ASyncSend,"AEP2");("CTR",Receive,"AEP1");("CTR",Read,"C");("CTR",Write,"C"); 276 map (fun l -> subjectReads g2 l) (nodes g2);; 277 map (fun l-> subjectAffects g2 l) (nodes g2);; 288 nodes g2;; 290 map (fun l -> subjectReads g2 l) (nodes g2);; 291 map (fun l-> subjectAffects g2 l) (nodes g2);; [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | graph_display.scala | 53 (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | graph_display.scala | 53 (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | concrltl2waaScript.sml | 541 >> qabbrev_tac `g2 = (��ls2 e1 sofar. 546 >- (`MEM y (FOLDR (g2 (trans_concr f)) [] (trans_concr f'))` by ( 547 qunabbrev_tac `g1` >> qunabbrev_tac `g2` >> fs[] 549 >> `!ls1 ls2. (MEM y (FOLDR (g2 ls2) [] ls1)) ==> 556 >> qunabbrev_tac `g2` >> qunabbrev_tac `g1` >> fs[MEM_MAP] 627 (FOLDR (��e1 sofar. g2 ls2 e1 sofar) [] ls1)` by ( 629 >> qunabbrev_tac `g1` >> qunabbrev_tac `g2` 666 (FOLDR (��e1 sofar. g2 ls2 e1 sofar) [] ls1)` by ( 668 >> qunabbrev_tac `g1` >> qunabbrev_tac `g2` 750 in let g2 [all...] |
H A D | concrRepScript.sml | 771 ``!g1 g2. 772 set (graphStatesWithId g1) = set (graphStatesWithId g2) 773 ==> (set (graphStates g1) = set (graphStates g2))``, 776 >- (`MEM (q,r.frml) (graphStatesWithId g2)` 970 ``!g g2. (g.followers = g2.followers) 971 ��� (domain g.nodeInfo = domain g2.nodeInfo) 973 = first_flw_has_max_counter g2)``, 1092 ``!g g2 f. (wfg g ��� unique_node_formula g ��� (addFrmlToGraph g f = g2)) [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | afp.scala | 57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) => 58 try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | afp.scala | 57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) => 58 try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr_t.sml | 207 val (r,g2) = gfoldn (f c) g1 208 in (d (l,r),g2) end 212 val (y,g2) = gfoldn l g1 213 in (b (x,y),g2) end 283 val (r,g2) = gfoldn (f c) g1 284 in (d (l,r),g2) end 288 val (y,g2) = gfoldn l g1 289 in (b (x,y),g2) end
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | computer_imp.ml | 106 g2:^sigtri16,g3:^sigtri16,g4:^sigtri16,bus:^sig16) = 109 DEST_TRI16 (memout t U16 g0 t U16 g1 t U16 g2 t U16 g3 t U16 g4 t)" 118 ?g0 g1 g2 g3 g4 memout alu bus. 128 G2(acc,racc,g2) /\ 132 BUS(memout,g0,g1,g2,g3,g4,bus)"
|