equal
deleted
inserted
replaced
2103 val ten = @{cterm \"10::nat\"} |
2103 val ten = @{cterm \"10::nat\"} |
2104 val ctrm = Thm.apply (Thm.apply add two) ten |
2104 val ctrm = Thm.apply (Thm.apply add two) ten |
2105 in |
2105 in |
2106 Thm.prop_of (Thm.beta_conversion true ctrm) |
2106 Thm.prop_of (Thm.beta_conversion true ctrm) |
2107 end" |
2107 end" |
2108 "Const (\"Pure.eq\",\<dots>) $ |
2108 "Const (\"Pure.eq\",_) $ |
2109 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2109 (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ |
2110 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2110 (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} |
2111 |
2111 |
2112 or in the pretty-printed form |
2112 or in the pretty-printed form |
2113 |
2113 |
2114 @{ML_response_fake [display,gray] |
2114 @{ML_response_fake [display,gray] |
2115 "let |
2115 "let |