equal
deleted
inserted
replaced
12 Var "name" |
12 Var "name" |
13 | Fun "ty" "ty" |
13 | Fun "ty" "ty" |
14 and tys = |
14 and tys = |
15 All xs::"name fset" ty::"ty" bind (res) xs in ty |
15 All xs::"name fset" ty::"ty" bind (res) xs in ty |
16 |
16 |
|
17 thm ty_tys.distinct |
|
18 thm ty_tys.induct |
|
19 thm ty_tys.exhaust |
|
20 thm ty_tys.fv_defs |
|
21 thm ty_tys.bn_defs |
|
22 thm ty_tys.perm_simps |
|
23 thm ty_tys.eq_iff |
|
24 thm ty_tys.fv_bn_eqvt |
|
25 thm ty_tys.size_eqvt |
|
26 thm ty_tys.supports |
|
27 thm ty_tys.fsupp |
17 |
28 |
18 nominal_datatype ty2 = |
29 nominal_datatype ty2 = |
19 Var2 "name" |
30 Var2 "name" |
20 | Fun2 "ty2" "ty2" |
31 | Fun2 "ty2" "ty2" |
21 |
32 |
22 |
|
23 nominal_datatype tys2 = |
33 nominal_datatype tys2 = |
24 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
34 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
25 |
35 |
|
36 thm tys2.distinct |
|
37 thm tys2.induct |
|
38 thm tys2.exhaust |
|
39 thm tys2.fv_defs |
|
40 thm tys2.bn_defs |
|
41 thm tys2.perm_simps |
|
42 thm tys2.eq_iff |
|
43 thm tys2.fv_bn_eqvt |
|
44 thm tys2.size_eqvt |
|
45 thm tys2.supports |
|
46 thm tys2.fsupp |
|
47 |
|
48 |
|
49 text {* *} |
26 |
50 |
27 (* |
51 (* |
28 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} |
52 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} |
29 |
53 |
30 lemma strong_induct: |
54 lemma strong_induct: |