src/Pure/Isar/proof.ML
changeset 11985 06658189cd51
parent 11924 b6def266cbb9
child 11992 a39798b57344
equal deleted inserted replaced
11984:324f69149895 11985:06658189cd51
   121 (* type goal *)
   121 (* type goal *)
   122 
   122 
   123 datatype kind =
   123 datatype kind =
   124   Theorem of string * theory attribute list |    (*top-level theorem*)
   124   Theorem of string * theory attribute list |    (*top-level theorem*)
   125   Show of context attribute list |               (*intermediate result, solving subgoal*)
   125   Show of context attribute list |               (*intermediate result, solving subgoal*)
   126   Have of context attribute list ;               (*intermediate result*)
   126   Have of context attribute list;                (*intermediate result*)
   127 
   127 
   128 val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have";
   128 val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have";
   129 
   129 
   130 type goal =
   130 type goal =
   131  (kind *        (*result kind*)
   131  (kind *        (*result kind*)