Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export get_consumes;
authorwenzelm
Fri, 05 Oct 2007 22:00:17 +0200
changeset 24862 6b7258da912b
parent 24861 cc669ca5f382
child 24863 307b979b1f54
export get_consumes;
src/Pure/Isar/rule_cases.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/rule_cases.ML	Fri Oct 05 22:00:15 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Fri Oct 05 22:00:17 2007 +0200
@@ -33,6 +33,7 @@
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
   val add_consumes: int -> thm -> thm
+  val get_consumes: thm -> int
   val consumes: int -> attribute
   val consumes_default: int -> attribute
   val name: string list -> thm -> thm
isabelle