equal
deleted
inserted
replaced
36 |
36 |
37 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = |
37 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = |
38 struct |
38 struct |
39 |
39 |
40 val beta_rules = |
40 val beta_rules = |
41 @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ |
41 @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ |
42 @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'}; |
42 @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'}; |
43 |
43 |
44 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); |
44 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); |
45 |
45 |
46 val beta_tac = simp_tac beta_ss; |
46 val beta_tac = simp_tac beta_ss; |