equal
deleted
inserted
replaced
40 infix -->>; |
40 infix -->>; |
41 infix 9 `; |
41 infix 9 `; |
42 |
42 |
43 (************************** miscellaneous functions ***************************) |
43 (************************** miscellaneous functions ***************************) |
44 |
44 |
45 val simple_ss = |
45 val simple_ss = HOL_basic_ss addsimps simp_thms; |
46 HOL_basic_ss addsimps simp_thms; |
46 |
47 |
47 val beta_rules = |
48 val beta_ss = |
48 @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ |
49 HOL_basic_ss |
49 @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; |
50 addsimps simp_thms |
50 |
51 addsimps [@{thm beta_cfun}] |
51 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); |
52 addsimprocs [@{simproc cont_proc}]; |
|
53 |
52 |
54 fun define_consts |
53 fun define_consts |
55 (specs : (binding * term * mixfix) list) |
54 (specs : (binding * term * mixfix) list) |
56 (thy : theory) |
55 (thy : theory) |
57 : (term list * thm list) * theory = |
56 : (term list * thm list) * theory = |