# HG changeset patch # User wenzelm # Date 975370222 -3600 # Node ID a0483268262d7bc621803aa2e83d1bcdc7e403b3 # Parent 7934b0fa8dccd05e157882d17a47d6fd625fb36f added "consumes" attribute; diff -r 7934b0fa8dcc -r a0483268262d src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Nov 28 01:09:40 2000 +0100 +++ b/src/Pure/Isar/attrib.ML Tue Nov 28 01:10:22 2000 +0100 @@ -262,6 +262,7 @@ (* rule cases *) +fun consumes x = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes) x; fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x; fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x; @@ -294,6 +295,7 @@ ("standard", (standard, standard), "result put into standard form"), ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"), ("no_vars", (no_vars, no_vars), "frozen schematic vars"), + ("consumes", (consumes, consumes), "number of consumed facts"), ("case_names", (case_names, case_names), "named rule cases"), ("params", (params, params), "named rule parameters"), ("exported", (exported_global, exported_local), "theorem exported from context")];