src/Pure/Isar/calculation.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18947 de38ee3654d4
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -9,11 +9,11 @@
     1.4  sig
     1.5    val print_rules: Context.generic -> unit
     1.6    val get_calculation: Proof.state -> thm list option
     1.7 -  val trans_add: Context.generic attribute
     1.8 -  val trans_del: Context.generic attribute
     1.9 -  val sym_add: Context.generic attribute
    1.10 -  val sym_del: Context.generic attribute
    1.11 -  val symmetric: Context.generic attribute
    1.12 +  val trans_add: attribute
    1.13 +  val trans_del: attribute
    1.14 +  val sym_add: attribute
    1.15 +  val sym_del: attribute
    1.16 +  val symmetric: attribute
    1.17    val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.18    val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.19    val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.20 @@ -60,9 +60,8 @@
    1.21  val calculationN = "calculation";
    1.22  
    1.23  fun put_calculation calc =
    1.24 -  `Proof.level #-> (fn lev =>
    1.25 -    Proof.map_context (Context.the_proof o
    1.26 -        CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
    1.27 +  `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
    1.28 +     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
    1.29    #> Proof.put_thms (calculationN, calc);
    1.30  
    1.31  
    1.32 @@ -71,20 +70,20 @@
    1.33  
    1.34  (* add/del rules *)
    1.35  
    1.36 -val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
    1.37 -val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
    1.38 +val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
    1.39 +val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
    1.40  
    1.41  val sym_add =
    1.42 -  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
    1.43 +  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule)
    1.44    #> ContextRules.elim_query NONE;
    1.45  val sym_del =
    1.46 -  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
    1.47 +  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
    1.48    #> ContextRules.rule_del;
    1.49  
    1.50  
    1.51  (* symmetric *)
    1.52  
    1.53 -val symmetric = Attrib.rule (fn x => fn th =>
    1.54 +val symmetric = Thm.rule_attribute (fn x => fn th =>
    1.55    (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
    1.56      ([th'], _) => th'
    1.57    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    1.58 @@ -98,12 +97,12 @@
    1.59  
    1.60  val _ = Context.add_setup
    1.61   (Attrib.add_attributes
    1.62 -   [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
    1.63 -    ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
    1.64 -    ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #>
    1.65 +   [("trans", trans_att, "declaration of transitivity rule"),
    1.66 +    ("sym", sym_att, "declaration of symmetry rule"),
    1.67 +    ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
    1.68    PureThy.add_thms
    1.69 -   [(("", transitive_thm), [Attrib.theory trans_add]),
    1.70 -    (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
    1.71 +   [(("", transitive_thm), [trans_add]),
    1.72 +    (("", symmetric_thm), [sym_add])] #> snd);
    1.73  
    1.74  
    1.75