export thisN
authorkleing
Tue, 13 Apr 2004 07:45:07 +0200
changeset 14548 e1a196985fc8
parent 14547 e0c0179100c9
child 14549 ea6e18e5c7a9
export thisN
src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 13 07:25:46 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 13 07:45:07 2004 +0200
@@ -122,6 +122,7 @@
   val begin_block: state -> state
   val end_block: state -> state Seq.seq
   val next_block: state -> state
+  val thisN: string
 end;
 
 structure Proof: PROOF =