src/Pure/Isar/method.ML
changeset 6091 e3cdbd929a24
parent 5921 50005d6ba609
child 6104 55c7f8f0bb4d
     1.1 --- a/src/Pure/Isar/method.ML	Tue Jan 12 13:39:41 1999 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Jan 12 13:40:08 1999 +0100
     1.3 @@ -14,16 +14,16 @@
     1.4  signature METHOD =
     1.5  sig
     1.6    include BASIC_METHOD
     1.7 -  val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * tthm list) list) Seq.seq
     1.8 -  val METHOD: (tthm list -> tactic) -> Proof.method
     1.9 +  val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * thm list) list) Seq.seq
    1.10 +  val METHOD: (thm list -> tactic) -> Proof.method
    1.11    val METHOD0: tactic -> Proof.method
    1.12    val fail: Proof.method
    1.13    val succeed: Proof.method
    1.14    val trivial: Proof.method
    1.15    val assumption: Proof.method
    1.16    val forward_chain: thm list -> thm list -> thm Seq.seq
    1.17 -  val rule_tac: tthm list -> tthm list -> int -> tactic
    1.18 -  val rule: tthm list -> Proof.method
    1.19 +  val rule_tac: thm list -> thm list -> int -> tactic
    1.20 +  val rule: thm list -> Proof.method
    1.21    exception METHOD_FAIL of (string * Position.T) * exn
    1.22    val method: theory -> Args.src -> Proof.context -> Proof.method
    1.23    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
    1.24 @@ -40,7 +40,7 @@
    1.25      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.26    val only_sectioned_args: (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.27      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.28 -  val thms_args: (tthm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.29 +  val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.30    datatype text =
    1.31      Basic of (Proof.context -> Proof.method) |
    1.32      Source of Args.src |
    1.33 @@ -59,7 +59,7 @@
    1.34    val trivial_proof: Proof.state -> Proof.state Seq.seq
    1.35    val default_proof: Proof.state -> Proof.state Seq.seq
    1.36    val qed: bstring option -> theory attribute list option -> Proof.state
    1.37 -    -> theory * (string * string * tthm)
    1.38 +    -> theory * (string * string * thm)
    1.39    val setup: (theory -> theory) list
    1.40  end;
    1.41  
    1.42 @@ -86,10 +86,8 @@
    1.43  
    1.44  fun trivial_tac [] = K all_tac
    1.45    | trivial_tac facts =
    1.46 -      let
    1.47 -        val thms = Attribute.thms_of facts;
    1.48 -        val r = ~ (length facts);
    1.49 -      in metacuts_tac thms THEN' rotate_tac r end;
    1.50 +      let val r = ~ (length facts);
    1.51 +      in metacuts_tac facts THEN' rotate_tac r end;
    1.52  
    1.53  val trivial = METHOD (ALLGOALS o trivial_tac);
    1.54  val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
    1.55 @@ -109,10 +107,10 @@
    1.56  
    1.57  fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
    1.58  
    1.59 -fun rule_tac rules [] = resolve_tac (Attribute.thms_of rules)
    1.60 +fun rule_tac rules [] = resolve_tac rules
    1.61    | rule_tac erules facts =
    1.62        let
    1.63 -        val rules = forward_chain (Attribute.thms_of facts) (Attribute.thms_of erules);
    1.64 +        val rules = forward_chain facts erules;
    1.65          fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules);
    1.66        in tac end;
    1.67  
    1.68 @@ -209,7 +207,7 @@
    1.69  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
    1.70  fun thmss ss = Scan.repeat (thms ss) >> flat;
    1.71  
    1.72 -fun apply att (ctxt, ths) = Attribute.applys ((ctxt, ths), [att]);
    1.73 +fun apply att (ctxt, ths) = Thm.applys_attributes ((ctxt, ths), [att]);
    1.74  
    1.75  fun section ss = (sect ss -- thmss ss) :-- (fn (att, ths) => Scan.depend (fn ctxt =>
    1.76    Scan.succeed (apply att (ctxt, ths)))) >> #2;