equal
deleted
inserted
replaced
28 |
28 |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
31 |
31 |
32 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") |
32 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") |
33 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
33 [[[], [], [(NONE, 0,1)]], [[], []] ] *} |
34 print_theorems |
34 print_theorems |
35 |
35 |
36 notation |
36 notation |
37 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
37 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
38 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
38 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |