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