equal
deleted
inserted
replaced
7 text {* type schemes *} |
7 text {* type schemes *} |
8 datatype ty = |
8 datatype ty = |
9 Var "name" |
9 Var "name" |
10 | Fun "ty" "ty" |
10 | Fun "ty" "ty" |
11 |
11 |
12 setup {* snd o define_raw_perms ["ty"] ["TySch.ty"] *} |
12 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} |
13 print_theorems |
13 print_theorems |
14 |
14 |
15 datatype tyS = |
15 datatype tyS = |
16 All "name set" "ty" |
16 All "name set" "ty" |
17 |
17 |
18 setup {* snd o define_raw_perms ["tyS"] ["TySch.tyS"] *} |
18 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} |
19 print_theorems |
19 print_theorems |
20 |
20 |
21 local_setup {* snd o define_fv_alpha "TySch.ty" [[[[]], [[], []]]] *} |
21 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") |
|
22 [[[[]], [[], []]]] *} |
22 print_theorems |
23 print_theorems |
23 |
24 |
24 (* |
25 (* |
25 Doesnot work yet since we do not refer to fv_ty |
26 Doesnot work yet since we do not refer to fv_ty |
26 local_setup {* define_raw_fv "TySch.tyS" [[[[], []]]] *} |
27 local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *} |
27 print_theorems |
28 print_theorems |
28 *) |
29 *) |
29 |
30 |
30 primrec |
31 primrec |
31 fv_tyS |
32 fv_tyS |