match_bind: 'as' patterns;
authorwenzelm
Thu Nov 19 11:49:09 1998 +0100 (1998-11-19 ago)
changeset 5938fe7640933a47
parent 5937 a777d702e81f
child 5939 2d7c7a4fcd8a
match_bind: 'as' patterns;
statements: 'is' patterns;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Nov 19 11:47:56 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Nov 19 11:49:09 1998 +0100
     1.3 @@ -21,12 +21,13 @@
     1.4    val have_facts: (string * Args.src list) * (string * Args.src list) list
     1.5      -> ProofHistory.T -> ProofHistory.T
     1.6    val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
     1.7 -  val match_bind: (string * string) list -> ProofHistory.T -> ProofHistory.T
     1.8 -  val theorem: string -> Args.src list -> string -> theory -> ProofHistory.T
     1.9 -  val lemma: string -> Args.src list -> string -> theory -> ProofHistory.T
    1.10 -  val assume: string -> Args.src list -> string list -> ProofHistory.T -> ProofHistory.T
    1.11 -  val show: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    1.12 -  val have: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    1.13 +  val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
    1.14 +  val theorem: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
    1.15 +  val lemma: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
    1.16 +  val assume: string -> Args.src list -> (string * string list) list
    1.17 +    -> ProofHistory.T -> ProofHistory.T
    1.18 +  val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    1.19 +  val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    1.20    val chain: ProofHistory.T -> ProofHistory.T
    1.21    val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
    1.22    val begin_block: ProofHistory.T -> ProofHistory.T