equal
deleted
inserted
replaced
15 |
15 |
16 |
16 |
17 thm Maybe.distinct |
17 thm Maybe.distinct |
18 thm Maybe.induct |
18 thm Maybe.induct |
19 thm Maybe.exhaust |
19 thm Maybe.exhaust |
|
20 thm Maybe.strong_exhaust |
20 thm Maybe.fv_defs |
21 thm Maybe.fv_defs |
21 thm Maybe.bn_defs |
22 thm Maybe.bn_defs |
22 thm Maybe.perm_simps |
23 thm Maybe.perm_simps |
23 thm Maybe.eq_iff |
24 thm Maybe.eq_iff |
24 thm Maybe.fv_bn_eqvt |
25 thm Maybe.fv_bn_eqvt |
25 thm Maybe.size_eqvt |
26 thm Maybe.size_eqvt |
26 thm Maybe.supp |
27 thm Maybe.supp |
27 |
28 |
28 (* |
29 (* |
29 using a datatype inside a nominal_datatype |
30 using a datatype inside a nominal_datatype |
|
31 |
|
32 the datatype needs to be shown to be an instance |
|
33 of the pure class (this is usually trivial) |
30 *) |
34 *) |
31 |
35 |
32 atom_decl name |
36 atom_decl name |
33 |
37 |
34 datatype foo = Foo | Bar |
38 datatype foo = Foo | Bar |
53 |
57 |
54 |
58 |
55 thm baz.distinct |
59 thm baz.distinct |
56 thm baz.induct |
60 thm baz.induct |
57 thm baz.exhaust |
61 thm baz.exhaust |
|
62 thm baz.strong_exhaust |
58 thm baz.fv_defs |
63 thm baz.fv_defs |
59 thm baz.bn_defs |
64 thm baz.bn_defs |
60 thm baz.perm_simps |
65 thm baz.perm_simps |
61 thm baz.eq_iff |
66 thm baz.eq_iff |
62 thm baz.fv_bn_eqvt |
67 thm baz.fv_bn_eqvt |