equal
deleted
inserted
replaced
119 (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm |
119 (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm |
120 | _ => Conv.all_conv ctm |
120 | _ => Conv.all_conv ctm |
121 end |
121 end |
122 |
122 |
123 val unfold_ret_val_invs = Conv.bottom_conv |
123 val unfold_ret_val_invs = Conv.bottom_conv |
124 (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy |
124 (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy |
125 val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv) |
125 val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv) |
126 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} |
126 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} |
127 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy |
127 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy |
128 val beta_conv = Thm.beta_conversion true |
128 val beta_conv = Thm.beta_conversion true |
129 val eq_thm = |
129 val eq_thm = |