changeset 2288 | 3b83960f9544 |
parent 2163 | 5dc48e1af733 |
--- a/Nominal/Ex/Test.thy Wed May 19 12:44:03 2010 +0100 +++ b/Nominal/Ex/Test.thy Thu May 20 21:23:53 2010 +0100 @@ -13,6 +13,7 @@ thm fv_trm_raw.simps[no_vars] *) + (* This file contains only the examples that are not supposed to work yet. *) @@ -29,7 +30,6 @@ | Ap "trm" "trm list" | Lm x::"name" t::"trm" bind x in t - (* thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]