typedef: export result;
authorwenzelm
Tue Oct 16 17:55:53 2001 +0200 (2001-10-16)
changeset 1180750a36627e6d6
parent 11806 e1fd22a657ae
child 11808 c724a9093ebe
typedef: export result;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Oct 16 17:55:38 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Oct 16 17:55:53 2001 +0200
     1.3 @@ -11,11 +11,13 @@
     1.4    val quiet_mode: bool ref
     1.5    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     1.6    val add_typedef: string -> bstring * string list * mixfix ->
     1.7 +    string -> string list -> thm list -> tactic option -> theory -> theory * thm
     1.8 +  val add_typedef_no_result: string -> bstring * string list * mixfix ->
     1.9      string -> string list -> thm list -> tactic option -> theory -> theory
    1.10    val add_typedef_i: string -> bstring * string list * mixfix ->
    1.11 -    term -> string list -> thm list -> tactic option -> theory -> theory
    1.12 +    term -> string list -> thm list -> tactic option -> theory -> theory * thm
    1.13    val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
    1.14 -    term -> string list -> thm list -> tactic option -> theory -> theory
    1.15 +    term -> string list -> thm list -> tactic option -> theory -> theory * thm
    1.16    val typedef_proof:
    1.17      (string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text
    1.18      -> bool -> theory -> ProofHistory.T
    1.19 @@ -208,11 +210,12 @@
    1.20    let
    1.21      val (cset, goal, _, typedef_att) = prepare_typedef prep_term no_def name typ set None thy;
    1.22      val result = prove_nonempty thy cset goal (names, thms, tac);
    1.23 -  in (thy, result) |> typedef_att |> #1 end;
    1.24 +  in (thy, result) |> typedef_att end;
    1.25  
    1.26  val add_typedef = gen_add_typedef read_term false;
    1.27  val add_typedef_i = gen_add_typedef cert_term false;
    1.28  val add_typedef_i_no_def = gen_add_typedef cert_term true;
    1.29 +fun add_typedef_no_result x y z = #1 oooo add_typedef x y z;
    1.30  
    1.31  
    1.32  (* typedef_proof interface *)