/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | ellipticTools.sml | 27 (* Subtype context. *) 30 val context = field_context; value 31 val context = subtypeTools.add_reduction2 curve_field context; value 32 val context = subtypeTools.add_reduction2 curve_a1_carrier context; value 33 val context = subtypeTools.add_reduction2 curve_a2_carrier context; value 34 val context = subtypeTools.add_reduction2 curve_a3_carrier context; value 35 val context = subtypeTools.add_reduction2 curve_a4_carrier context; value 36 val context = subtypeTools.add_reduction2 curve_a6_carrier context; value 37 val context = subtypeTools.add_reduction2 curve_zero_carrier context; value 38 val context = subtypeTools.add_reduction2 curve_neg_carrier context; value 39 val context = subtypeTools.add_reduction2 curve_double_carrier context; value 40 val context = subtypeTools.add_reduction2 curve_add_carrier context; value 41 val context = subtypeTools.add_rewrite2 curve_double_zero context; value 42 val context = subtypeTools.add_rewrite2 curve_add_lzero context; value 43 val context = subtypeTools.add_rewrite2 curve_add_lneg context; value 44 val context = subtypeTools.add_rewrite2 curve_add_rzero context; value 45 val context = subtypeTools.add_rewrite2 curve_add_rneg context; value [all...] |
H A D | groupTools.sml | 76 (* Subtype context. *) 79 val context = subtypeTools.empty2; value 80 val context = subtypeTools.add_judgement2 AbelianGroup_Group context; value 81 val context = subtypeTools.add_judgement2 FiniteGroup_Group context; value 82 val context = subtypeTools.add_judgement2 FiniteAbelianGroup_FiniteGroup context; value 83 val context = value 84 subtypeTools.add_judgement2 FiniteAbelianGroup_AbelianGroup context; 85 val context = subtypeTools.add_reduction2 group_id_carrier context; value 86 val context = subtypeTools.add_reduction2 group_inv_carrier context; value 87 val context = subtypeTools.add_reduction2 group_mult_carrier context; value 88 val context = subtypeTools.add_rewrite2 group_lid context; value 89 val context = subtypeTools.add_rewrite2 group_linv context; value 90 val context = subtypeTools.add_rewrite2'' group_assoc context; value 91 val context = subtypeTools.add_rewrite2 group_rinv context; value 92 val context = subtypeTools.add_rewrite2 group_rid context; value 93 val context = subtypeTools.add_rewrite2' group_lcancel context; value 94 val context = subtypeTools.add_rewrite2' group_lcancel_id context; value 95 val context = subtypeTools.add_rewrite2' group_rcancel context; value 96 val context = subtypeTools.add_rewrite2' group_rcancel_id context; value 97 val context = subtypeTools.add_rewrite2' group_inv_cancel context; value 98 val context = subtypeTools.add_rewrite2 group_inv_inv context; value 99 val context = subtypeTools.add_rewrite2 group_inv_id context; value 100 val context = subtypeTools.add_rewrite2'' group_inv_mult context; value 101 val context = subtypeTools.add_reduction2 group_exp_carrier context; value 102 val context = subtypeTools.add_rewrite2 group_id_exp context; value 103 val context = subtypeTools.add_conversion2'' group_ac_conv context; value 104 val context = subtypeTools.add_reduction2 trivial_group context; value 105 val context = subtypeTools.add_reduction2 add_mod context; value 106 val context = subtypeTools.add_judgement2 Prime_Nonzero context; value 107 val context = subtypeTools.add_reduction2 mult_mod context; value [all...] |
H A D | fieldTools.sml | 967 fun field_div_elim_ss context = 991 val {simplify = alg_ss, ...} = subtypeTools.simpset2 context 1134 fun field_poly_ss context term_normalize_ths = 1154 val {simplify = alg_ss, ...} = subtypeTools.simpset2 context 1194 fun field_poly_basis_ss context = 1216 val {simplify = alg_ss, ...} = subtypeTools.simpset2 context 1222 (* Subtype context. *) 1225 val context = group_context; value 1226 val context = subtypeTools.add_rewrite2'' field_sub_def context; value 1227 val context = subtypeTools.add_judgement2 FiniteField_Field context; value 1228 val context = subtypeTools.add_judgement2 field_nonzero_carrier context; value 1229 val context = subtypeTools.add_reduction2 field_zero_carrier context; value 1230 val context = subtypeTools.add_rewrite2 field_one_zero context; value 1231 val context = subtypeTools.add_reduction2 field_one_nonzero context; value 1232 val context = subtypeTools.add_reduction2 field_neg_carrier context; value 1233 val context = subtypeTools.add_reduction2 field_add_carrier context; value 1234 val context = subtypeTools.add_rewrite2'' field_add_assoc context; value 1235 val context = subtypeTools.add_rewrite2 field_num_zero context; value 1236 val context = subtypeTools.add_rewrite2 field_add_lzero context; value 1237 val context = subtypeTools.add_rewrite2'' (GSYM field_num_one) context; value 1238 val context = subtypeTools.add_rewrite2 field_add_lzero' context; value 1239 val context = subtypeTools.add_rewrite2 field_add_rzero context; value 1240 val context = subtypeTools.add_rewrite2 field_add_rzero' context; value 1241 val context = subtypeTools.add_rewrite2 field_lneg context; value 1242 val context = subtypeTools.add_rewrite2 field_lneg' context; value 1243 val context = subtypeTools.add_rewrite2 field_rneg context; value 1244 val context = subtypeTools.add_rewrite2 field_rneg' context; value 1245 val context = subtypeTools.add_rewrite2' field_add_lcancel context; value 1246 val context = subtypeTools.add_rewrite2' field_add_rcancel context; value 1247 val context = subtypeTools.add_reduction2 field_inv_nonzero context; value 1248 val context = subtypeTools.add_rewrite2 field_mult_lzero context; value 1249 val context = subtypeTools.add_rewrite2 field_mult_lzero' context; value 1250 val context = subtypeTools.add_rewrite2 field_mult_rzero context; value 1251 val context = subtypeTools.add_rewrite2 field_mult_rzero' context; value 1252 val context = subtypeTools.add_reduction2 field_mult_nonzero context; value 1253 val context = subtypeTools.add_reduction2 field_mult_carrier context; value 1254 val context = subtypeTools.add_rewrite2'' field_mult_assoc context; value 1255 val context = subtypeTools.add_rewrite2' field_entire context; value 1256 val context = subtypeTools.add_rewrite2 field_mult_lone context; value 1257 val context = subtypeTools.add_rewrite2 field_mult_lone' context; value 1258 val context = subtypeTools.add_rewrite2 field_mult_rone context; value 1259 val context = subtypeTools.add_rewrite2 field_mult_rone' context; value 1260 val context = subtypeTools.add_rewrite2 field_linv context; value 1261 val context = subtypeTools.add_rewrite2 field_linv' context; value 1262 val context = subtypeTools.add_rewrite2 field_rinv context; value 1263 val context = subtypeTools.add_rewrite2 field_rinv' context; value 1264 val context = subtypeTools.add_rewrite2' field_mult_lcancel context; value 1265 val context = subtypeTools.add_rewrite2' field_mult_rcancel context; value 1266 val context = subtypeTools.add_rewrite2 field_neg_neg context; value 1267 val context = subtypeTools.add_rewrite2 field_neg_cancel context; value 1268 val context = subtypeTools.add_rewrite2 field_neg_zero context; value 1269 val context = subtypeTools.add_rewrite2 field_mult_lneg context; value 1270 val context = subtypeTools.add_rewrite2 field_mult_rneg context; value 1271 val context = subtypeTools.add_rewrite2'' field_inv_mult context; value 1272 val context = subtypeTools.add_reduction2 field_exp_carrier context; value 1273 val context = subtypeTools.add_reduction2 field_exp_nonzero context; value 1274 val context = subtypeTools.add_reduction2 field_num_carrier context; value 1275 val context = subtypeTools.add_rewrite2 field_inv_one context; value 1276 val context = subtypeTools.add_rewrite2 field_exp_zero context; value 1277 val context = subtypeTools.add_rewrite2 field_exp_one context; value 1278 val context = subtypeTools.add_rewrite2'' field_neg_add context; value 1279 val context = subtypeTools.add_rewrite2 field_num_add context; value 1280 val context = subtypeTools.add_rewrite2'' field_num_add' context; value 1281 val context = subtypeTools.add_rewrite2 field_num_mult context; value 1282 val context = subtypeTools.add_rewrite2'' field_num_mult' context; value 1283 val context = subtypeTools.add_rewrite2 field_num_exp context; value 1284 val context = subtypeTools.add_rewrite2'' field_single_add_single context; value 1285 val context = subtypeTools.add_rewrite2'' field_single_add_single' context; value 1286 val context = subtypeTools.add_rewrite2'' field_single_add_mult context; value 1287 val context = subtypeTools.add_rewrite2'' field_single_add_mult' context; value 1288 val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult context; value 1289 val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult' context; value 1290 val context = subtypeTools.add_rewrite2'' field_mult_add_mult context; value 1291 val context = subtypeTools.add_rewrite2'' field_mult_add_mult' context; value 1292 val context = subtypeTools.add_rewrite2'' field_mult_add_neg context; value 1293 val context = subtypeTools.add_rewrite2'' field_mult_add_neg' context; value 1294 val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult context; value 1295 val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult' context; value 1296 val context = subtypeTools.add_rewrite2'' field_neg_add_neg context; value 1297 val context = subtypeTools.add_rewrite2'' field_neg_add_neg' context; value 1298 val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult context; value 1299 val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult' context; value 1300 val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult context; value 1301 val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult' context; value 1302 val context = subtypeTools.add_rewrite2'' field_single_mult_single context; value 1303 val context = subtypeTools.add_rewrite2'' field_single_mult_single' context; value 1304 val context = subtypeTools.add_rewrite2'' field_single_mult_exp context; value 1305 val context = subtypeTools.add_rewrite2'' field_single_mult_exp' context; value 1306 val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp context; value 1307 val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp' context; value 1308 val context = subtypeTools.add_rewrite2'' field_exp_mult_exp context; value 1309 val context = subtypeTools.add_rewrite2'' field_exp_mult_exp' context; value 1310 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv context; value 1311 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv' context; value 1312 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp context; value 1313 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp' context; value 1314 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv context; value 1315 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv' context; value 1316 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp context; value 1317 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp' context; value 1318 val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp context; value 1319 val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp' context; value 1320 val context = subtypeTools.add_rewrite2 field_one_exp context; value 1321 val context = subtypeTools.add_rewrite2 field_zero_exp context; value 1322 val context = subtypeTools.add_rewrite2 field_exp_eq_zero context; value 1323 val context = subtypeTools.add_rewrite2'' field_exp_neg context; value 1324 val context = subtypeTools.add_rewrite2'' field_exp_exp context; value 1325 val context = subtypeTools.add_conversion2'' field_sub_eq_zero_r_conv context; value 1326 val context = subtypeTools.add_conversion2'' field_sub_eq_zero_l_conv context; value 1327 val context = subtypeTools.add_rewrite2 field_inv_inv context; value 1328 val context = subtypeTools.add_reduction2 field_sub_carrier context; value 1329 val context = subtypeTools.add_reduction2 field_neg_nonzero context; value 1330 val context = subtypeTools.add_rewrite2'' field_inv_neg context; value 1331 val context = subtypeTools.add_rewrite2'' field_exp_mult context; value 1332 val context = subtypeTools.add_rewrite2'' field_exp_inv context; value 1333 val context = subtypeTools.add_conversion2'' field_add_ac_conv context; value 1334 val context = subtypeTools.add_conversion2'' field_mult_ac_conv context; value 1335 val context = subtypeTools.add_reduction2 field_div_carrier context; value 1336 val context = subtypeTools.add_reduction2 field_div_nonzero context; value 1337 val context = subtypeTools.add_rewrite2 field_inv_eq_zero context; value 1338 val context = subtypeTools.add_rewrite2 field_div_eq_zero context; value 1339 val context = subtypeTools.add_judgement2 GF_in_carrier_imp context; value 1340 val context = subtypeTools.add_reduction2 GF context; value [all...] |
H A D | subtypeTools.sig | 46 type context type 48 val empty : context 50 val add_rewrite : Thm.thm -> context -> context 52 val add_conversion : named_conv -> context -> context 54 val add_reduction : Thm.thm -> context -> context 56 val add_judgement : Thm.thm -> context -> context [all...] |
H A D | fieldScript.sml | 56 (* The subtype context. *) 59 val context = group_context; value 60 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 204 val context = subtypeTools.add_rewrite2'' field_sub_def context; value 205 (*val context = subtypeTools.add_rewrite2'' field_div_def context;*) 206 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 465 val context = subtypeTools.add_judgement2 FiniteField_Field context; value 473 val context = subtypeTools.add_judgement2 field_nonzero_carrier context; value 494 val context = subtypeTools.add_reduction2 field_zero_carrier context; value 516 val context = subtypeTools.add_rewrite2 field_one_zero context; value 530 val context = subtypeTools.add_reduction2 field_one_nonzero context; value 539 val context = subtypeTools.add_reduction2 field_neg_carrier context; value 548 val context = subtypeTools.add_reduction2 field_add_carrier context; value 559 val context = subtypeTools.add_rewrite2'' field_add_assoc context; value 581 val context = subtypeTools.add_rewrite2 field_num_zero context; value 593 val context = subtypeTools.add_rewrite2 field_add_lzero context; value 602 val context = subtypeTools.add_rewrite2'' (GSYM field_num_one) context; value 610 val context = subtypeTools.add_rewrite2 field_add_lzero' context; value 618 val context = subtypeTools.add_rewrite2 field_add_rzero context; value 626 val context = subtypeTools.add_rewrite2 field_add_rzero' context; value 639 val context = subtypeTools.add_rewrite2 field_lneg context; value 649 val context = subtypeTools.add_rewrite2 field_lneg' context; value 658 val context = subtypeTools.add_rewrite2 field_rneg context; value 668 val context = subtypeTools.add_rewrite2 field_rneg' context; value 687 val context = subtypeTools.add_rewrite2' field_add_lcancel context; value 702 val context = subtypeTools.add_rewrite2' field_add_rcancel context; value 718 val context = subtypeTools.add_reduction2 field_inv_nonzero context; value 727 val context = subtypeTools.add_rewrite2 field_mult_lzero context; value 736 val context = subtypeTools.add_rewrite2 field_mult_lzero' context; value 814 val context = subtypeTools.add_rewrite2 field_mult_rzero context; value 823 val context = subtypeTools.add_rewrite2 field_mult_rzero' context; value 838 val context = subtypeTools.add_reduction2 field_mult_nonzero context; value 854 val context = subtypeTools.add_reduction2 field_mult_carrier context; value 875 val context = subtypeTools.add_rewrite2'' field_mult_assoc context; value 921 val context = subtypeTools.add_rewrite2' field_entire context; value 937 val context = subtypeTools.add_rewrite2 field_mult_lone context; value 945 val context = subtypeTools.add_rewrite2 field_mult_lone' context; value 953 val context = subtypeTools.add_rewrite2 field_mult_rone context; value 961 val context = subtypeTools.add_rewrite2 field_mult_rone' context; value 974 val context = subtypeTools.add_rewrite2 field_linv context; value 984 val context = subtypeTools.add_rewrite2 field_linv' context; value 994 val context = subtypeTools.add_rewrite2 field_rinv context; value 1004 val context = subtypeTools.add_rewrite2 field_rinv' context; value 1032 val context = subtypeTools.add_rewrite2' field_mult_lcancel context; value 1047 val context = subtypeTools.add_rewrite2' field_mult_rcancel context; value 1056 val context = subtypeTools.add_rewrite2 field_neg_neg context; value 1066 val context = subtypeTools.add_rewrite2 field_neg_cancel context; value 1123 val context = subtypeTools.add_rewrite2 field_neg_zero context; value 1159 val context = subtypeTools.add_rewrite2 field_mult_lneg context; value 1168 val context = subtypeTools.add_rewrite2 field_mult_rneg context; value 1190 val context = subtypeTools.add_rewrite2'' field_inv_mult context; value 1200 val context = subtypeTools.add_reduction2 field_exp_carrier context; value 1211 val context = subtypeTools.add_reduction2 field_exp_nonzero context; value 1221 val context = subtypeTools.add_reduction2 field_num_carrier context; value 1257 val context = subtypeTools.add_rewrite2 field_inv_one context; value 1265 val context = subtypeTools.add_rewrite2 field_exp_zero context; value 1274 val context = subtypeTools.add_rewrite2 field_exp_one context; value 1295 val context = subtypeTools.add_rewrite2'' field_neg_add context; value 1321 val context = subtypeTools.add_rewrite2 field_num_add context; value 1331 val context = subtypeTools.add_rewrite2'' field_num_add' context; value 1343 val context = subtypeTools.add_rewrite2 field_num_mult context; value 1353 val context = subtypeTools.add_rewrite2'' field_num_mult' context; value 1364 val context = subtypeTools.add_rewrite2 field_num_exp context; value 1373 val context = subtypeTools.add_rewrite2'' field_single_add_single context; value 1383 val context = subtypeTools.add_rewrite2'' field_single_add_single' context; value 1394 val context = subtypeTools.add_rewrite2'' field_single_add_mult context; value 1404 val context = subtypeTools.add_rewrite2'' field_single_add_mult' context; value 1420 val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult context; value 1435 val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult' context; value 1451 val context = subtypeTools.add_rewrite2'' field_mult_add_mult context; value 1462 val context = subtypeTools.add_rewrite2'' field_mult_add_mult' context; value 1477 val context = subtypeTools.add_rewrite2'' field_mult_add_neg context; value 1491 val context = subtypeTools.add_rewrite2'' field_mult_add_neg' context; value 1528 val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult context; value 1543 val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult' context; value 1553 val context = subtypeTools.add_rewrite2'' field_neg_add_neg context; value 1563 val context = subtypeTools.add_rewrite2'' field_neg_add_neg' context; value 1575 val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult context; value 1586 val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult' context; value 1602 val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult context; value 1613 val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult' context; value 1621 val context = subtypeTools.add_rewrite2'' field_single_mult_single context; value 1630 val context = subtypeTools.add_rewrite2'' field_single_mult_single' context; value 1639 val context = subtypeTools.add_rewrite2'' field_single_mult_exp context; value 1649 val context = subtypeTools.add_rewrite2'' field_single_mult_exp' context; value 1663 val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp context; value 1676 val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp' context; value 1691 val context = subtypeTools.add_rewrite2'' field_exp_mult_exp context; value 1701 val context = subtypeTools.add_rewrite2'' field_exp_mult_exp' context; value 1715 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv context; value 1728 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv' context; value 1762 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp context; value 1776 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp' context; value 1786 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv context; value 1796 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv' context; value 1807 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp context; value 1818 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp' context; value 1834 val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp context; value 1845 val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp' context; value 1855 val context = subtypeTools.add_rewrite2 field_one_exp context; value 1869 val context = subtypeTools.add_rewrite2 field_zero_exp context; value 1882 val context = subtypeTools.add_rewrite2 field_exp_eq_zero context; value 1894 val context = subtypeTools.add_rewrite2'' field_exp_neg context; value 1908 val context = subtypeTools.add_rewrite2'' field_exp_exp context; value 1958 val context = subtypeTools.add_conversion2'' field_sub_eq_zero_r_conv context; value 1959 val context = subtypeTools.add_conversion2'' field_sub_eq_zero_l_conv context; value 1976 val context = subtypeTools.add_rewrite2 field_inv_inv context; value 1985 val context = subtypeTools.add_reduction2 field_sub_carrier context; value 2004 val context = subtypeTools.add_reduction2 field_neg_nonzero context; value 2023 val context = subtypeTools.add_rewrite2'' field_inv_neg context; value 2042 val context = subtypeTools.add_rewrite2'' field_exp_mult context; value 2055 val context = subtypeTools.add_rewrite2'' field_exp_inv context; value 2111 val context = subtypeTools.add_conversion2'' field_add_ac_conv context; value 2163 val context = subtypeTools.add_conversion2'' field_mult_ac_conv context; value 2215 val context = subtypeTools.add_reduction2 field_div_carrier context; value 2224 val context = subtypeTools.add_reduction2 field_div_nonzero context; value 2380 val context = subtypeTools.add_rewrite2 field_inv_eq_zero context; value 2390 val context = subtypeTools.add_rewrite2 field_div_eq_zero context; value 2552 val context = subtypeTools.add_judgement2 GF_in_carrier_imp context; value 2684 val context = subtypeTools.add_reduction2 GF context; value [all...] |
H A D | ellipticTools.sig | 21 (* Subtype context. *)
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | registerset.c | 16 void Arch_initContext(user_context_t* context) argument 18 Mode_initContext(context); 19 context->registers[TLS_BASE] = 0; 20 context->registers[Error] = 0; 21 context->registers[FaultIP] = 0; 22 context->registers[NextIP] = 0; /* overwritten by setNextPC() later on */ 23 context->registers[CS] = SEL_CS_3; 24 context->registers[FLAGS] = FLAGS_USER_DEFAULT; 25 context->registers[SS] = SEL_DS_3; 27 Arch_initFpuContext(context); [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/machine/ |
H A D | registerset.c | 30 void Mode_initContext(user_context_t* context) argument 32 context->registers[RAX] = 0; 33 context->registers[RBX] = 0; 34 context->registers[RCX] = 0; 35 context->registers[RDX] = 0; 36 context->registers[RSI] = 0; 37 context->registers[RDI] = 0; 38 context->registers[RBP] = 0; 39 context->registers[R8] = 0; 40 context [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/groups/ |
H A D | arithContext.sig | 6 type context = subtypeTools.context type 12 val arith_c : context;
|
H A D | finite_groupContext.sig | 6 type context = subtypeTools.context type 12 val finite_group_c : context;
|
H A D | groupContext.sig | 6 type context = subtypeTools.context type 12 val group_c : context;
|
H A D | mult_groupContext.sig | 6 type context = subtypeTools.context type 12 val mult_group_c : context;
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/machine/ |
H A D | registerset.c | 30 void Mode_initContext(user_context_t* context) argument 32 context->registers[EAX] = 0; 33 context->registers[EBX] = 0; 34 context->registers[ECX] = 0; 35 context->registers[EDX] = 0; 36 context->registers[ESI] = 0; 37 context->registers[EDI] = 0; 38 context->registers[EBP] = 0; 39 context->registers[DS] = SEL_DS_3; 40 context [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/formalize/ |
H A D | boolContext.sig | 6 type context = subtypeTools.context type 13 val bool_c : context;
|
H A D | listContext.sig | 6 type context = subtypeTools.context type 13 val list_c : context;
|
H A D | numContext.sig | 6 type context = subtypeTools.context type 13 val num_c : context;
|
H A D | pred_setContext.sig | 6 type context = subtypeTools.context type 13 val pred_set_c : context;
|
H A D | realContext.sig | 6 type context = subtypeTools.context type 13 val real_c : context;
|
/seL4-l4v-10.1.1/HOL4/examples/miller/subtypes/ |
H A D | subtypeTools.sig | 44 (* Subtype context operations *) 64 type context type 85 val new_context : unit -> context 86 val pp_context : context PP.pprinter 87 val context_subtypes : context -> subtype_context 88 val context_add_fact : vthm -> context -> context 89 val context_add_element : context_element -> context -> context 90 val context_add_elements : context_element list -> context [all...] |
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Traverse.sig | 13 * type context 15 * Each reducer collects the working context on its own. 16 * A context object is the current state of a single reducer. 19 type context = exn (* well known SML hack to allow any kind of data *) type 27 * Each reducer manages its own storage of the working context (of one 44 * be used to solve side conditions in context. 49 * context: 50 * The reducer's current view of the context, as 61 * addcontext: routine is invoked every time more context is added 64 * initial: The inital context [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | editor.scala | 21 def current_node(context: Context): Option[Document.Node.Name] 22 def current_node_snapshot(context: Context): Option[Document.Snapshot] 24 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] 39 def follow(context: Context): Unit
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | editor.scala | 21 def current_node(context: Context): Option[Document.Node.Name] 22 def current_node_snapshot(context: Context): Option[Document.Snapshot] 24 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] 39 def follow(context: Context): Unit
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | gr-sig.sml | 54 type ('a,'b) context = 'b out * node * 'a * 'b out 55 type ('a,'b) decomp = ('a,'b) context * ('a,'b) graph 66 val embed : ('a,'b) context * ('a,'b) graph -> ('a,'b) graph 75 val context : node * ('a,'b) graph -> ('a,'b) context value 80 val ufold : (('a,'b) context * 'c -> 'c) -> 'c -> ('a,'b) graph -> 'c 81 val gfold : (('a,'b) context -> node list) -> ('a * 'c -> 'd) -> 101 type 'a context = node list * node * 'a * node list 102 type 'a decomp = 'a context * 'a graph 113 val embed : 'a context * ' 118 val context : node * 'a graph -> 'a context value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr-sig.sml | 54 type ('a,'b) context = 'b out * node * 'a * 'b out 55 type ('a,'b) decomp = ('a,'b) context * ('a,'b) graph 66 val embed : ('a,'b) context * ('a,'b) graph -> ('a,'b) graph 75 val context : node * ('a,'b) graph -> ('a,'b) context value 80 val ufold : (('a,'b) context * 'c -> 'c) -> 'c -> ('a,'b) graph -> 'c 81 val gfold : (('a,'b) context -> node list) -> ('a * 'c -> 'd) -> 101 type 'a context = node list * node * 'a * node list 102 type 'a decomp = 'a context * 'a graph 113 val embed : 'a context * ' 118 val context : node * 'a graph -> 'a context value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr-sig.sml | 54 type ('a,'b) context = 'b out * node * 'a * 'b out 55 type ('a,'b) decomp = ('a,'b) context * ('a,'b) graph 66 val embed : ('a,'b) context * ('a,'b) graph -> ('a,'b) graph 75 val context : node * ('a,'b) graph -> ('a,'b) context value 80 val ufold : (('a,'b) context * 'c -> 'c) -> 'c -> ('a,'b) graph -> 'c 81 val gfold : (('a,'b) context -> node list) -> ('a * 'c -> 'd) -> 101 type 'a context = node list * node * 'a * node list 102 type 'a decomp = 'a context * 'a graph 113 val embed : 'a context * ' 118 val context : node * 'a graph -> 'a context value [all...] |