changeset 11985 | 06658189cd51 |
parent 11924 | b6def266cbb9 |
child 11992 | a39798b57344 |
--- a/src/Pure/Isar/proof.ML Tue Oct 30 17:30:21 2001 +0100 +++ b/src/Pure/Isar/proof.ML Tue Oct 30 17:33:03 2001 +0100 @@ -123,7 +123,7 @@ datatype kind = Theorem of string * theory attribute list | (*top-level theorem*) Show of context attribute list | (*intermediate result, solving subgoal*) - Have of context attribute list ; (*intermediate result*) + Have of context attribute list; (*intermediate result*) val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have";