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 (set+) xs in ty |
15 All xs::"name fset" ty::"ty" binds (set+) xs in ty |
16 |
16 |
17 ML {* |
17 ML {* |
18 get_all_info @{context} |
18 get_all_info @{context} |
19 *} |
19 *} |
20 |
20 |
280 nominal_datatype ty2 = |
280 nominal_datatype ty2 = |
281 Var2 "name" |
281 Var2 "name" |
282 | Fun2 "ty2" "ty2" |
282 | Fun2 "ty2" "ty2" |
283 |
283 |
284 nominal_datatype tys2 = |
284 nominal_datatype tys2 = |
285 All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty |
285 All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty |
286 |
286 |
287 thm tys2.distinct |
287 thm tys2.distinct |
288 thm tys2.induct tys2.strong_induct |
288 thm tys2.induct tys2.strong_induct |
289 thm tys2.exhaust tys2.strong_exhaust |
289 thm tys2.exhaust tys2.strong_exhaust |
290 thm tys2.fv_defs |
290 thm tys2.fv_defs |