src/Pure/Isar/local_defs.ML
changeset 20306 614b7e6c6276
parent 20224 9c40a144ee0e
child 20887 ec9a1bb086da
     1.1 --- a/src/Pure/Isar/local_defs.ML	Wed Aug 02 22:26:59 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Aug 02 22:27:00 2006 +0200
     1.3 @@ -7,23 +7,22 @@
     1.4  
     1.5  signature LOCAL_DEFS =
     1.6  sig
     1.7 -  val cert_def: ProofContext.context -> term -> (string * typ) * term
     1.8 +  val cert_def: Proof.context -> term -> (string * typ) * term
     1.9    val abs_def: term -> (string * typ) * term
    1.10 -  val mk_def: ProofContext.context -> (string * term) list -> term list
    1.11 +  val mk_def: Proof.context -> (string * term) list -> term list
    1.12    val def_export: Assumption.export
    1.13 -  val add_def: string * term -> ProofContext.context ->
    1.14 -    ((string * typ) * thm) * ProofContext.context
    1.15 +  val add_def: string * term -> Proof.context -> ((string * typ) * thm) * Proof.context
    1.16    val print_rules: Context.generic -> unit
    1.17    val defn_add: attribute
    1.18    val defn_del: attribute
    1.19    val meta_rewrite_rule: Context.generic -> thm -> thm
    1.20 -  val unfold: ProofContext.context -> thm list -> thm -> thm
    1.21 -  val unfold_goals: ProofContext.context -> thm list -> thm -> thm
    1.22 -  val unfold_tac: ProofContext.context -> thm list -> tactic
    1.23 -  val fold: ProofContext.context -> thm list -> thm -> thm
    1.24 -  val fold_tac: ProofContext.context -> thm list -> tactic
    1.25 -  val derived_def: ProofContext.context -> bool -> term ->
    1.26 -    ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
    1.27 +  val unfold: Proof.context -> thm list -> thm -> thm
    1.28 +  val unfold_goals: Proof.context -> thm list -> thm -> thm
    1.29 +  val unfold_tac: Proof.context -> thm list -> tactic
    1.30 +  val fold: Proof.context -> thm list -> thm -> thm
    1.31 +  val fold_tac: Proof.context -> thm list -> tactic
    1.32 +  val derived_def: Proof.context -> bool -> term ->
    1.33 +    ((string * typ) * term) * (Proof.context -> term -> thm -> thm)
    1.34  end;
    1.35  
    1.36  structure LocalDefs: LOCAL_DEFS =
    1.37 @@ -67,11 +66,11 @@
    1.38    -----------
    1.39        B t
    1.40  *)
    1.41 -fun def_export _ cprops thm =
    1.42 +fun def_export _ defs thm =
    1.43    thm
    1.44 -  |> Drule.implies_intr_list cprops
    1.45 -  |> Drule.generalize ([], map head_of_def cprops)
    1.46 -  |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
    1.47 +  |> Drule.implies_intr_list defs
    1.48 +  |> Drule.generalize ([], map head_of_def defs)
    1.49 +  |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
    1.50  
    1.51  
    1.52  (* add defs *)