changeset 61476 | 1884c40f1539 |
parent 60758 | d8d85a8172b5 |
child 61799 | 4cf66f21b764 |
--- a/src/HOL/Presburger.thy Sun Oct 18 20:48:24 2015 +0200 +++ b/src/HOL/Presburger.thy Sun Oct 18 21:30:01 2015 +0200 @@ -400,7 +400,7 @@ val delN = "del" val elimN = "elim" val any_keyword = keyword addN || keyword delN || simple_keyword elimN - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm) in Scan.optional (simple_keyword elimN >> K false) true -- Scan.optional (keyword addN |-- thms) [] --