changeset 286 | 804fbb227568 |
parent 283 | c4d821c6309d |
child 293 | 1a4e5b94293b |
--- a/thys/Simplifying.thy Wed May 16 20:58:39 2018 +0100 +++ b/thys/Simplifying.thy Wed Aug 15 13:48:57 2018 +0100 @@ -230,7 +230,7 @@ qed qed - +(* fun simp2_ALT where "simp2_ALT ZERO r2 seen = (r2, seen)" | "simp2_ALT r1 ZERO seen = (r1, seen)" @@ -367,5 +367,5 @@ apply(simp add: Sequ_def) apply(auto)[1] oops - +*) end \ No newline at end of file