src/Pure/Isar/calculation.ML
changeset 15801 d2f5ca3c048d
parent 15570 8d8c70b41bab
child 15973 5fd94d84470f
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Apr 21 22:00:28 2005 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Apr 21 22:02:06 2005 +0200
     1.3 @@ -25,7 +25,6 @@
     1.4      -> Proof.state -> Proof.state Seq.seq
     1.5    val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
     1.6    val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
     1.7 -  val setup: (theory -> theory) list
     1.8  end;
     1.9  
    1.10  structure Calculation: CALCULATION =
    1.11 @@ -54,6 +53,7 @@
    1.12  end;
    1.13  
    1.14  structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    1.15 +val _ = Context.add_setup [GlobalCalculation.init];
    1.16  val print_global_rules = GlobalCalculation.print;
    1.17  
    1.18  
    1.19 @@ -69,6 +69,7 @@
    1.20  end;
    1.21  
    1.22  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    1.23 +val _ = Context.add_setup [LocalCalculation.init];
    1.24  val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
    1.25  val print_local_rules = LocalCalculation.print;
    1.26  
    1.27 @@ -129,6 +130,16 @@
    1.28   (Attrib.add_del_args sym_add_global sym_del_global,
    1.29    Attrib.add_del_args sym_add_local sym_del_local);
    1.30  
    1.31 +val _ = Context.add_setup
    1.32 + [Attrib.add_attributes
    1.33 +   [("trans", trans_attr, "declaration of transitivity rule"),
    1.34 +    ("sym", sym_attr, "declaration of symmetry rule"),
    1.35 +    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
    1.36 +      "resolution with symmetry rule")],
    1.37 +  #1 o PureThy.add_thms
    1.38 +   [(("", transitive_thm), [trans_add_global]),
    1.39 +    (("", symmetric_thm), [sym_add_global])]];
    1.40 +
    1.41  
    1.42  
    1.43  (** proof commands **)
    1.44 @@ -207,18 +218,4 @@
    1.45  fun ultimately print = collect true print;
    1.46  
    1.47  
    1.48 -
    1.49 -(** theory setup **)
    1.50 -
    1.51 -val setup =
    1.52 - [GlobalCalculation.init, LocalCalculation.init,
    1.53 -  Attrib.add_attributes
    1.54 -   [("trans", trans_attr, "declaration of transitivity rule"),
    1.55 -    ("sym", sym_attr, "declaration of symmetry rule"),
    1.56 -    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
    1.57 -      "resolution with symmetry rule")],
    1.58 -  #1 o PureThy.add_thms
    1.59 -   [(("", transitive_thm), [trans_add_global]),
    1.60 -    (("", symmetric_thm), [sym_add_global])]];
    1.61 -
    1.62  end;