20 "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. |
20 "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. |
21 |
21 |
22 lemma [code, code del]: |
22 lemma [code, code del]: |
23 "pred_of_set = pred_of_set" .. |
23 "pred_of_set = pred_of_set" .. |
24 |
24 |
25 |
|
26 lemma [code, code del]: |
|
27 "Cardinality.card' = Cardinality.card'" .. |
|
28 |
|
29 lemma [code, code del]: |
|
30 "Cardinality.finite' = Cardinality.finite'" .. |
|
31 |
|
32 lemma [code, code del]: |
|
33 "Cardinality.subset' = Cardinality.subset'" .. |
|
34 |
|
35 lemma [code, code del]: |
|
36 "Cardinality.eq_set = Cardinality.eq_set" .. |
|
37 |
|
38 |
|
39 lemma [code, code del]: |
25 lemma [code, code del]: |
40 "acc = acc" .. |
26 "acc = acc" .. |
|
27 |
|
28 lemmas [code del] = |
|
29 finite_set_code finite_coset_code |
|
30 equal_set_code |
41 |
31 |
42 (* |
32 (* |
43 If the code generation ends with an exception with the following message: |
33 If the code generation ends with an exception with the following message: |
44 '"List.set" is not a constructor, on left hand side of equation: ...', |
34 '"List.set" is not a constructor, on left hand side of equation: ...', |
45 the code equation in question has to be either deleted (like many others in this file) |
35 the code equation in question has to be either deleted (like many others in this file) |