| /seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
| H A D | syntax.tex | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | annotatedIR.sml | 142 val context = G.context(n,gr) value
[all...] |
| H A D | funCall.sml | [all...] |
| H A D | gr-sig.sml | 75 val context : node * ('a,'b) graph -> ('a,'b) context value
118 val context : node * 'a graph -> 'a context value
[all...] |
| H A D | gr_t.sml | 131 fun context _ = raise NotImplemented function
193 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
269 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | annotatedIR.sml | 132 val context = G.context(n,gr) value
[all...] |
| H A D | funCall.sml | [all...] |
| H A D | gr-sig.sml | 75 val context : node * ('a,'b) graph -> ('a,'b) context value
118 val context : node * 'a graph -> 'a context value
[all...] |
| H A D | gr_t.sml | 131 fun context _ = raise NotImplemented function
193 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
269 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | annotatedIR.sml | 132 val context = G.context(n,gr) value
[all...] |
| H A D | funCall.sml | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | gr-sig.sml | 75 val context : node * ('a,'b) graph -> ('a,'b) context value
118 val context : node * 'a graph -> 'a context value
[all...] |
| H A D | gr_t.sml | 131 fun context _ = raise NotImplemented function
193 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
269 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | ellipticScript.sml | 59 val context = field_context; value
673 val context = subtypeTools.add_reduction2 curve_field context; value
681 val context = subtypeTools.add_reduction2 curve_a1_carrier context; value
689 val context value
697 val context = subtypeTools.add_reduction2 curve_a3_carrier context; value
705 val context = subtypeTools.add_reduction2 curve_a4_carrier context; value
713 val context = subtypeTools.add_reduction2 curve_a6_carrier context; value
1137 val context = subtypeTools.add_reduction2 curve_zero_carrier context; value
1151 val context = subtypeTools.add_reduction2 curve_neg_carrier context; value
1182 val context = subtypeTools.add_reduction2 curve_double_carrier context; value
1217 val context = subtypeTools.add_reduction2 curve_add_carrier context; value
1229 val context = subtypeTools.add_rewrite2 curve_double_zero context; value
1241 val context = subtypeTools.add_rewrite2 curve_add_lzero context; value
1262 val context = subtypeTools.add_rewrite2 curve_add_lneg context; value
1310 val context = subtypeTools.add_rewrite2 curve_add_rzero context; value
1319 val context = subtypeTools.add_rewrite2 curve_add_rneg context; value
1418 val context = subtypeTools.add_rewrite2 example_prime_def context; value
1421 val context = subtypeTools.add_rewrite2 example_field_def context; value
1429 val context = value
1437 val context = value
1451 val context = subtypeTools.add_reduction2 example_curve context; value
[all...] |
| H A D | ellipticTools.sml | 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 | elliptic_exampleScript.sml | 43 val context = elliptic_context; value
95 val context = subtypeTools.add_reduction2 example1_prime context; value
102 val context = subtypeTools.add_reduction2 example1_field context; value
115 val context value
[all...] |
| H A D | fieldScript.sml | 59 val context = group_context; value
204 val context = subtypeTools.add_rewrite2'' field_sub_def context; value
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 | fieldTools.sml | 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 | groupScript.sml | 52 val context = subtypeTools.empty2; value
551 val context = subtypeTools.add_judgement2 AbelianGroup_Group context; value
559 val context = subtypeTools.add_judgement2 FiniteGroup_Group context; value
567 val context value
575 val context = value
596 val context = subtypeTools.add_reduction2 group_id_carrier context; value
604 val context = subtypeTools.add_reduction2 group_inv_carrier context; value
612 val context = subtypeTools.add_reduction2 group_mult_carrier context; value
620 val context = subtypeTools.add_rewrite2 group_lid context; value
628 val context = subtypeTools.add_rewrite2 group_linv context; value
637 val context = subtypeTools.add_rewrite2'' group_assoc context; value
697 val context = subtypeTools.add_rewrite2 group_rinv context; value
724 val context = subtypeTools.add_rewrite2 group_rid context; value
747 val context = subtypeTools.add_rewrite2' group_lcancel context; value
767 val context = subtypeTools.add_rewrite2' group_lcancel_id context; value
800 val context = subtypeTools.add_rewrite2' group_rcancel context; value
820 val context = subtypeTools.add_rewrite2' group_rcancel_id context; value
848 val context = subtypeTools.add_rewrite2' group_inv_cancel context; value
861 val context = subtypeTools.add_rewrite2 group_inv_inv context; value
889 val context = subtypeTools.add_rewrite2 group_inv_id context; value
931 val context = subtypeTools.add_rewrite2'' group_inv_mult context; value
942 val context = subtypeTools.add_reduction2 group_exp_carrier context; value
952 val context = subtypeTools.add_rewrite2 group_id_exp context; value
1073 val context = subtypeTools.add_conversion2'' group_ac_conv context; value
1135 val context = subtypeTools.add_reduction2 trivial_group context; value
1426 val context = subtypeTools.add_reduction2 add_mod context; value
1448 val context = subtypeTools.add_judgement2 Prime_Nonzero context; value
1514 val context = subtypeTools.add_reduction2 mult_mod context; value
[all...] |
| H A D | groupTools.sml | 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
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 | subtypeTools.sig | 46 type context type
[all...] |
| H A D | subtypeTools.sml | 273 datatype context = type
403 val {context, solver = _, conv = _, relation = _, stack = _} = dproc_context value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/miller/formalize/ |
| H A D | boolContext.sig | 6 type context = subtypeTools.context type
|
| H A D | listContext.sig | 6 type context = subtypeTools.context type
|
| H A D | numContext.sig | 6 type context = subtypeTools.context type
|