/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | closure.sml | 12 let g1 x = x + y in 14 (twice(g1,z),twice(g2,z))`; 26 val g1'_def = Define ` 27 g1' (x,y) = x + y`; 35 G1 y -> g1'(i,y) || 44 let g1:clos = G1 y in 46 (twice1(g1,z),twice1(g2,z))`; 57 twice_def, dispatch_def,g1'_def, g2'_def]
|
H A D | gr_t.sml | 206 let val (c as (_,_,l,_),g1) = match (v,g) 207 val (r,g2) = gfoldn (f c) g1 211 let val (x,g1) = gfold1 v g 212 val (y,g2) = gfoldn l g1 282 let val (c as (_,_,l,_),g1) = match (v,g) 283 val (r,g2) = gfoldn (f c) g1 287 let val (x,g1) = gfold1 v g 288 val (y,g2) = gfoldn l g1
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | closure.sml | 12 let g1 x = x + y in 14 (twice(g1,z),twice(g2,z))`; 26 val g1'_def = Define ` 27 g1' (x,y) = x + y`; 35 G1 y -> g1'(i,y) || 44 let g1:clos = G1 y in 46 (twice1(g1,z),twice1(g2,z))`; 57 RW_TAC std_ss [g1'_def, g2'_def]
|
H A D | gr_t.sml | 206 let val (c as (_,_,l,_),g1) = match (v,g) 207 val (r,g2) = gfoldn (f c) g1 211 let val (x,g1) = gfold1 v g 212 val (y,g2) = gfoldn l g1 282 let val (c as (_,_,l,_),g1) = match (v,g) 283 val (r,g2) = gfoldn (f c) g1 287 let val (x,g1) = gfold1 v g 288 val (y,g2) = gfoldn l g1
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | closure.sml | 12 let g1 x = x + y in 14 (twice(g1,z),twice(g2,z))`; 26 val g1'_def = Define ` 27 g1' (x,y) = x + y`; 35 G1 y -> g1'(i,y) || 44 let g1:clos = G1 y 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 | 26 int g1(int *iptr) function 38 return g1(&global1.array[0][1]);
|
H A D | automatic_modifies.c | 23 void g1(int i) function 35 g1(i);
|
H A D | jiraver439.c | 20 unsigned g1(void) 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) 165 ++ Suff `divides p (gcd (gord G g1) (gord G g2))` 175 ++ Q.PAT_X_ASSUM `!g1 [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)``, 509 (Cases_on `?g. g IN lcoset G g1 H 517 ++ Suff `!v. v IN lcoset G g1 H = v IN lcoset G g2 H` 523 ++ Q.SPEC_TAC (`g1`, `g1`) [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)`; 252 /\ (STATESAT (M,s) (E g1) = ?PI. (PI IS_FAIR_PATH_IN M) /\ 253 (PI STATE_NO 0 = s) /\ PATHSAT(M,PI) g1) [all...] |
/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. 120 (inj_pair f1 g1) ==> 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 f [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | encap1.lisp | 40 ; theorem (presumably proved by showing the existence of the g1 guaranteed by 41 ; "some g1" below). 42 ; Definition. g1 = some g1 . forall x . (integerp (g1 x)) 43 ; |- forall x . |= (integerp (g1 x)) 45 ((g1 (x) t)) 46 (local (defun g1 (x) 49 (defthm integerp-g1 50 (integerp (g1 [all...] |
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/ |
H A D | pattern_matchingScript.sml | 57 val _ = def "g1" 58 `(g1 (0,x) = x) /\ 59 (g1 (x,0) = x)`;
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/encap/ |
H A D | example.lisp | 38 ; theorem (presumably proved by showing the existence of the g1 guaranteed by 39 ; "some g1" below). 40 ; Definition. g1 = some g1 . forall x . (integerp (g1 x)) 41 ; |- forall x . |= (integerp (g1 x)) 43 ((g1 (x) t)) 44 (local (defun g1 (x) 47 (defthm integerp-g1 48 (integerp (g1 [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/sparc/ |
H A D | v8.S | 192 ld [%g2+FFI_TRAMPOLINE_SIZE], %g1 193 ld [%g1+4], %g1 194 sll %g1, 3, %g1 195 add %g1, STACKFRAME, %g1 196 ! %g1 == STACKFRAME + 8*nargs 197 neg %g1 198 save %sp, %g1, [all...] |
/seL4-l4v-10.1.1/HOL4/src/boss/ |
H A D | selftest.sml | 86 val (g1:goal) = ([boolSyntax.mk_conj(P,Q)], boolSyntax.mk_neg(P)) value 89 (match1_tac test1 g1) 98 val res1' = test_assert (equal [g1] o #1) 99 (first_match_tac test2 g1)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | graph_display.scala | 52 case (g1, ((ident, _), parents)) => 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 | 52 case (g1, ((ident, _), parents)) => 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 | concrRepScript.sml | 771 ``!g1 g2. 772 set (graphStatesWithId g1) = set (graphStatesWithId g2) 773 ==> (set (graphStates g1) = set (graphStates g2))``, 781 >- (`MEM (q,r.frml) (graphStatesWithId g1)` 1209 ``!g1 g2 f props. (wfg g1 1210 ��� addFrmlToGraph g1 f = g2 1211 ��� unique_node_formula g1) 1212 ==> !x. extractTrans g1 x = extractTrans g2 x``, 1214 >> `!id. (IS_SOME (lookup id g1 [all...] |
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibSimple.sml | 123 val g1 = sys avoid sgty_exists v tm1 value 124 in inst_guess g1 [tm1, tm2] SIMPLE_GUESS_EXISTS_AND_1 end 137 val g1 = sys avoid sgty_forall v tm1 value 138 in inst_guess g1 [tm1, tm2] SIMPLE_GUESS_FORALL_OR_1 end 151 val g1 = sys avoid sgty_exists v tm1 value 152 in inst_guess g1 [tm1, tm2] SIMPLE_GUESS_FORALL_IMP_1 end 165 val g1 = GEN v' g0 value 170 val thm' = HO_MATCH_MP thm0 g1 178 val g1 = GEN v' g0 value 183 val thm' = HO_MATCH_MP thm0 g1 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/ |
H A D | word8Script.sml | 224 `(a,b,c,d,e,f,g,h) XOR8 (a1,b1,c1,d1,e1,f1,g1,h1) 232 g XOR g1, 239 `(a,b,c,d,e,f,g,h) AND8 (a1,b1,c1,d1,e1,f1,g1,h1) 247 g /\ g1,
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | afp.scala | 56 (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) => 57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | afp.scala | 56 (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) => 57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr_t.sml | 206 let val (c as (_,_,l,_),g1) = match (v,g) 207 val (r,g2) = gfoldn (f c) g1 211 let val (x,g1) = gfold1 v g 212 val (y,g2) = gfoldn l g1 282 let val (c as (_,_,l,_),g1) = match (v,g) 283 val (r,g2) = gfoldn (f c) g1 287 let val (x,g1) = gfold1 v g 288 val (y,g2) = gfoldn l g1
|