equal
deleted
inserted
replaced
10 |
10 |
11 nominal_datatype ty = |
11 nominal_datatype ty = |
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 (set+) xs in ty |
16 |
16 |
17 thm ty_tys.distinct |
17 thm ty_tys.distinct |
18 thm ty_tys.induct |
18 thm ty_tys.induct |
19 thm ty_tys.inducts |
19 thm ty_tys.inducts |
20 thm ty_tys.exhaust ty_tys.strong_exhaust |
20 thm ty_tys.exhaust ty_tys.strong_exhaust |
33 nominal_datatype ty2 = |
33 nominal_datatype ty2 = |
34 Var2 "name" |
34 Var2 "name" |
35 | Fun2 "ty2" "ty2" |
35 | Fun2 "ty2" "ty2" |
36 |
36 |
37 nominal_datatype tys2 = |
37 nominal_datatype tys2 = |
38 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
38 All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty |
39 |
39 |
40 thm tys2.distinct |
40 thm tys2.distinct |
41 thm tys2.induct tys2.strong_induct |
41 thm tys2.induct tys2.strong_induct |
42 thm tys2.exhaust tys2.strong_exhaust |
42 thm tys2.exhaust tys2.strong_exhaust |
43 thm tys2.fv_defs |
43 thm tys2.fv_defs |