clarified order of arith rules;
authorwenzelm
Sat Aug 16 16:45:39 2014 +0200 (2014-08-16)
changeset 57955f28337c2c0a8
parent 57954 c52223cd1003
child 57956 3ab5d15fac6b
clarified order of arith rules;
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/lin_arith.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 16:18:39 2014 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 16:45:39 2014 +0200
     1.3 @@ -863,7 +863,7 @@
     1.4      val simpset_ctxt =
     1.5        put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
     1.6    in
     1.7 -    Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith})
     1.8 +    Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}))
     1.9      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    1.10      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.11      THEN_ALL_NEW simp_tac simpset_ctxt
     2.1 --- a/src/HOL/Tools/arith_data.ML	Sat Aug 16 16:18:39 2014 +0200
     2.2 +++ b/src/HOL/Tools/arith_data.ML	Sat Aug 16 16:45:39 2014 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4      (Scan.succeed (fn ctxt =>
     2.5        METHOD (fn facts =>
     2.6          HEADGOAL
     2.7 -        (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
     2.8 +        (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
     2.9            THEN' verbose_arith_tac ctxt))))
    2.10      "various arithmetic decision procedures";
    2.11  
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Aug 16 16:18:39 2014 +0200
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Aug 16 16:45:39 2014 +0200
     3.3 @@ -796,7 +796,7 @@
     3.4  
     3.5  (* FIXME !?? *)
     3.6  fun add_arith_facts ctxt =
     3.7 -  Simplifier.add_prems (Named_Theorems.get ctxt @{named_theorems arith}) ctxt;
     3.8 +  Simplifier.add_prems (rev (Named_Theorems.get ctxt @{named_theorems arith})) ctxt;
     3.9  
    3.10  val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    3.11  
    3.12 @@ -889,7 +889,7 @@
    3.13    Method.setup @{binding linarith}
    3.14      (Scan.succeed (fn ctxt =>
    3.15        METHOD (fn facts =>
    3.16 -        HEADGOAL (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
    3.17 +        HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
    3.18            THEN' tac ctxt)))) "linear arithmetic" #>
    3.19    Arith_Data.add_tactic "linear arithmetic" gen_tac;
    3.20