| changeset 40326 | 73d45866dbda |
| parent 40322 | 707eb30e8a53 |
| child 40327 | 1dfdbd66093a |
--- a/src/HOLCF/ex/Pattern_Match.thy Fri Oct 29 16:24:07 2010 -0700 +++ b/src/HOLCF/ex/Pattern_Match.thy Fri Oct 29 16:51:40 2010 -0700 @@ -363,7 +363,7 @@ infix 9 ` ; val beta_rules = - @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ + @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);