| changeset 61337 | 4645502c3c64 |
| parent 60770 | 240563fbf41d |
| child 61395 | 4f8c2c4a0a8c |
--- a/src/ZF/Bin.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/ZF/Bin.thy Tue Oct 06 15:14:28 2015 +0200 @@ -700,7 +700,7 @@ text \<open>@{text combine_numerals_prod} (products of separate literals)\<close> lemma "#5 $* x $* #3 = y" apply simp oops -schematic_lemma "y2 $+ ?x42 = y $+ y2" apply simp oops +schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops