equal
deleted
inserted
replaced
8 |
8 |
9 datatype rtrm4 = |
9 datatype rtrm4 = |
10 rVr4 "name" |
10 rVr4 "name" |
11 | rAp4 "rtrm4" "rtrm4 list" |
11 | rAp4 "rtrm4" "rtrm4 list" |
12 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
12 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
13 print_theorems |
|
14 |
|
15 thm rtrm4.recs |
|
16 |
13 |
17 (* there cannot be a clause for lists, as *) |
14 (* there cannot be a clause for lists, as *) |
18 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
15 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
19 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} |
16 ML {* |
|
17 val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4"; |
|
18 val {descr, sorts, ...} = dtinfo; |
|
19 *} |
|
20 setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *} |
20 print_theorems |
21 print_theorems |
21 |
22 |
22 (* "repairing" of the permute function *) |
23 (* "repairing" of the permute function *) |
23 lemma repaired: |
24 lemma repaired: |
24 fixes ts::"rtrm4 list" |
25 fixes ts::"rtrm4 list" |