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>) $ |
2128 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2128 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2129 |
2129 |
2130 or in the pretty-printed form |
2130 or in the pretty-printed form |
2131 |
2131 |
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.capply (Thm.capply 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) |
2143 |> pretty_term ctxt |
2143 |> pretty_term ctxt |
2144 |> pwriteln |
2144 |> pwriteln |
2145 end" |
2145 end" |