equal
deleted
inserted
replaced
2176 in |
2176 in |
2177 Thm.prop_of (Thm.beta_conversion true ctrm) |
2177 Thm.prop_of (Thm.beta_conversion true ctrm) |
2178 end" |
2178 end" |
2179 "Const (\"==\",\<dots>) $ |
2179 "Const (\"==\",\<dots>) $ |
2180 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2180 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ |
2181 (Const (\"Algebras.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2181 (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} |
2182 |
2182 |
2183 The argument @{ML true} in @{ML beta_conversion in Thm} indicates that |
2183 The argument @{ML true} in @{ML beta_conversion in Thm} indicates that |
2184 the right-hand side should be fully beta-normalised. If instead |
2184 the right-hand side should be fully beta-normalised. If instead |
2185 @{ML false} is given, then only a single beta-reduction is performed |
2185 @{ML false} is given, then only a single beta-reduction is performed |
2186 on the outer-most level. |
2186 on the outer-most level. |