equal
deleted
inserted
replaced
2099 @{ML_response_fake [display,gray] |
2099 @{ML_response_fake [display,gray] |
2100 "let |
2100 "let |
2101 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2101 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2102 val two = @{cterm \"2::nat\"} |
2102 val two = @{cterm \"2::nat\"} |
2103 val ten = @{cterm \"10::nat\"} |
2103 val ten = @{cterm \"10::nat\"} |
2104 val ctrm = Thm.capply (Thm.capply add two) ten |
2104 val ctrm = Thm.apply (Thm.apply add two) ten |
2105 in |
2105 in |
2106 Thm.beta_conversion true ctrm |
2106 Thm.beta_conversion true ctrm |
2107 end" |
2107 end" |
2108 "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"} |
2108 "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"} |
2109 |
2109 |
2117 @{ML_response [display,gray] |
2117 @{ML_response [display,gray] |
2118 "let |
2118 "let |
2119 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2119 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2120 val two = @{cterm \"2::nat\"} |
2120 val two = @{cterm \"2::nat\"} |
2121 val ten = @{cterm \"10::nat\"} |
2121 val ten = @{cterm \"10::nat\"} |
2122 val ctrm = Thm.capply (Thm.capply add two) ten |
2122 val ctrm = Thm.apply (Thm.apply add two) ten |
2123 in |
2123 in |
2124 Thm.prop_of (Thm.beta_conversion true ctrm) |
2124 Thm.prop_of (Thm.beta_conversion true ctrm) |
2125 end" |
2125 end" |
2126 "Const (\"==\",\<dots>) $ |
2126 "Const (\"==\",\<dots>) $ |
2127 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2127 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2132 @{ML_response_fake [display,gray] |
2132 @{ML_response_fake [display,gray] |
2133 "let |
2133 "let |
2134 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2134 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
2135 val two = @{cterm \"2::nat\"} |
2135 val two = @{cterm \"2::nat\"} |
2136 val ten = @{cterm \"10::nat\"} |
2136 val ten = @{cterm \"10::nat\"} |
2137 val ctrm = Thm.capply (Thm.capply add two) ten |
2137 val ctrm = Thm.apply (Thm.apply add two) ten |
2138 val ctxt = @{context} |
2138 val ctxt = @{context} |
2139 |> Config.put eta_contract false |
2139 |> Config.put eta_contract false |
2140 |> Config.put show_abbrevs false |
2140 |> Config.put show_abbrevs false |
2141 in |
2141 in |
2142 Thm.prop_of (Thm.beta_conversion true ctrm) |
2142 Thm.prop_of (Thm.beta_conversion true ctrm) |
2185 |
2185 |
2186 @{ML_response_fake [display,gray] |
2186 @{ML_response_fake [display,gray] |
2187 "let |
2187 "let |
2188 val conv1 = Thm.beta_conversion false |
2188 val conv1 = Thm.beta_conversion false |
2189 val conv2 = Conv.rewr_conv @{thm true_conj1} |
2189 val conv2 = Conv.rewr_conv @{thm true_conj1} |
2190 val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"} |
2190 val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"} |
2191 in |
2191 in |
2192 (conv1 then_conv conv2) ctrm |
2192 (conv1 then_conv conv2) ctrm |
2193 end" |
2193 end" |
2194 "(\<lambda>x. x \<and> False) True \<equiv> False"} |
2194 "(\<lambda>x. x \<and> False) True \<equiv> False"} |
2195 |
2195 |