# HG changeset patch # User wenzelm # Date 1350399003 -7200 # Node ID 34437e7245cce7488d5825af90a74d55ff1d1ab3 # Parent b5fb6e7f8d819cd5ce2b43ec66cbad026e92cabc updated Toplevel.proofs; diff -r b5fb6e7f8d81 -r 34437e7245cc src/Doc/IsarImplementation/Integration.thy --- a/src/Doc/IsarImplementation/Integration.thy Tue Oct 16 15:14:12 2012 +0200 +++ b/src/Doc/IsarImplementation/Integration.thy Tue Oct 16 16:50:03 2012 +0200 @@ -154,7 +154,7 @@ Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) -> + @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> Toplevel.transition -> Toplevel.transition"} \\