equal
deleted
inserted
replaced
261 |
261 |
262 (*evaluate identity |
262 (*evaluate identity |
263 > reflI; |
263 > reflI; |
264 val it = "(?t = ?t) = True" |
264 val it = "(?t = ?t) = True" |
265 > val t = str2term "x = 0"; |
265 > val t = str2term "x = 0"; |
266 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t; |
266 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
267 |
267 |
268 > val t = str2term "1 = 0"; |
268 > val t = str2term "1 = 0"; |
269 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t; |
269 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
270 ----------- thus needs Rule.Eval ! |
270 ----------- thus needs Rule.Eval ! |
271 > val t = str2term "0 = 0"; |
271 > val t = str2term "0 = 0"; |
272 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t; |
272 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
273 > UnparseC.term t'; |
273 > UnparseC.term t'; |
274 val it = \<^const_name>\<open>True\<close> |
274 val it = \<^const_name>\<open>True\<close> |
275 |
275 |
276 val t = str2term "Not (x = 0)"; |
276 val t = str2term "Not (x = 0)"; |
277 atomt t; UnparseC.term t; |
277 atomt t; UnparseC.term t; |