src/Pure/Isar/proof.ML
changeset 11742 44034a6474e5
parent 11556 8e0768929662
child 11793 5f0ab6f5c280
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Oct 13 20:32:07 2001 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Oct 13 20:32:38 2001 +0200
     1.3 @@ -81,13 +81,9 @@
     1.4    val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     1.5      -> state -> state
     1.6    val invoke_case: string * context attribute list -> state -> state
     1.7 -  val theorem: bstring -> theory attribute list -> string * (string list * string list)
     1.8 -    -> theory -> state
     1.9 -  val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
    1.10 +  val theorem: string -> bstring -> theory attribute list -> string * (string list * string list)
    1.11      -> theory -> state
    1.12 -  val lemma: bstring -> theory attribute list -> string * (string list * string list)
    1.13 -    -> theory -> state
    1.14 -  val lemma_i: bstring -> theory attribute list -> term * (term list * term list)
    1.15 +  val theorem_i: string -> bstring -> theory attribute list -> term * (term list * term list)
    1.16      -> theory -> state
    1.17    val chain: state -> state
    1.18    val from_facts: thm list -> state -> state
    1.19 @@ -127,13 +123,11 @@
    1.20  (* type goal *)
    1.21  
    1.22  datatype kind =
    1.23 -  Theorem of theory attribute list |    (*top-level theorem*)
    1.24 -  Lemma of theory attribute list |      (*top-level lemma*)
    1.25 -  Show of context attribute list |      (*intermediate result, solving subgoal*)
    1.26 -  Have of context attribute list ;      (*intermediate result*)
    1.27 +  Theorem of string * theory attribute list |    (*top-level theorem*)
    1.28 +  Show of context attribute list |               (*intermediate result, solving subgoal*)
    1.29 +  Have of context attribute list ;               (*intermediate result*)
    1.30  
    1.31 -val kind_name =
    1.32 -  fn Theorem _ => "theorem" | Lemma _ => "lemma" | Show _ => "show" | Have _ => "have";
    1.33 +val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have";
    1.34  
    1.35  type goal =
    1.36   (kind *        (*result kind*)
    1.37 @@ -619,12 +613,10 @@
    1.38  
    1.39  (*global goals*)
    1.40  fun global_goal prepp kind name atts x thy =
    1.41 -  setup_goal I prepp kind Seq.single name atts x (init_state thy);
    1.42 +  setup_goal I prepp (curry Theorem kind) Seq.single name atts x (init_state thy);
    1.43  
    1.44 -val theorem = global_goal ProofContext.bind_propp_schematic Theorem;
    1.45 -val theorem_i = global_goal ProofContext.bind_propp_schematic_i Theorem;
    1.46 -val lemma = global_goal ProofContext.bind_propp_schematic Lemma;
    1.47 -val lemma_i = global_goal ProofContext.bind_propp_schematic_i Lemma;
    1.48 +val theorem = global_goal ProofContext.bind_propp_schematic;
    1.49 +val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
    1.50  
    1.51  
    1.52  (*local goals*)
    1.53 @@ -720,9 +712,7 @@
    1.54        |> curry Thm.name_thm full_name;
    1.55  
    1.56      val atts =
    1.57 -      (case kind of
    1.58 -        Theorem atts => atts
    1.59 -      | Lemma atts => atts @ [Drule.tag_lemma]
    1.60 +      (case kind of Theorem (s, atts) => atts @ [Drule.kind s]
    1.61        | _ => err_malformed "finish_global" state);
    1.62  
    1.63      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);