(*WN060306 from isabelle-users:

put expressions involving plus and minus into a canonical form. Here is a possible set of 

rules:

  add_assoc add_commute

  diff_def minus_add_distrib

  minus_minus minus_zero

===========================================================================*)

(*

 cd ~/Isabelle2002/src/HOL/Real

 grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml

 WN 9.8.02

ML> thy;

val it =

  {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type,

    Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion,

    NatDef, Nat, NatArith, Divides, Power, SetInterval, Finite_Set, Equiv,

    IntDef, Int, Datatype_Universe, Datatype, Numeral, Bin, IntArith,

    Wellfounded_Relations, Recdef, IntDiv, IntPower, NatBin, NatSimprocs,

    Relation_Power, PreList, List, Map, Hilbert_Choice, Main, Lubs, PNat, PRat,

    PReal, RealDef, RealOrd, RealInt, RealBin, RealArith0, RealArith,

    RComplete, RealAbs, RealPow, Ring_and_Field, Complex_Numbers, Real}

  : theory

theories with their respective theorems found by

grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml;

theories listed in the the order as found in Real.thy above

comments

    (**)"...theorem..."  : first choice for one of the rule-sets

    "...theorem..."(*??*): to be investigated

    "...theorem...       : just for documenting the contents

*)

Lubs.ML:qed -----------------------------------------------------------------

 "setleI";     "ALL y::?'a:?S::?'a set. y <= (?x::?'a) ==> ?S *<= ?x"

 "setleD";     "[| (?S::?'a set) *<= (?x::?'a); (?y::?'a) : ?S |] ==> ?y <= ?x"

 "setgeI";     "Ball (?S::?'a set) (op <= (?x::?'a)) ==> ?x <=* ?S"

 "setgeD";     "[| (?x::?'a) <=* (?S::?'a set); (?y::?'a) : ?S |] ==> ?x <= ?y"

 "leastPD1";

 "leastPD2";

 "leastPD3";

 "isLubD1";

 "isLubD1a";

 "isLub_isUb";

 "isLubD2";

 "isLubD3";

 "isLubI1";

 "isLubI2";

 "isUbD";

       	 "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |]

       	  ==> ?y <= ?x" "isUbD2";

 "isUbD2a";

 "isUbI";

 "isLub_le_isUb";

 "isLub_ubs";

PNat.ML:qed ------------------------------------------------------------------

 "pnat_fun_mono";          "mono (%X::nat set. {Suc (0::nat)} Un Suc ` X)"

 "one_RepI";               "Suc (0::nat) : pnat"

 "pnat_Suc_RepI";

 "two_RepI";

 "PNat_induct";

       	 "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat));

       	     !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i"

 "pnat_induct";

       	 "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |]

       	  ==> ?P (?n::pnat)"

 "pnat_diff_induct";

 "pnatE";

 "inj_on_Abs_pnat";

 "inj_Rep_pnat";

 "zero_not_mem_pnat";

 "mem_pnat_gt_zero";

 "gt_0_mem_pnat";

 "mem_pnat_gt_0_iff";

 "Rep_pnat_gt_zero";

 "pnat_add_commute";        "(?x::pnat) + (?y::pnat) = ?y + ?x"

 "Collect_pnat_gt_0";

 "pSuc_not_one";

 "inj_pSuc"; 

 "pSuc_pSuc_eq";

 "n_not_pSuc_n";

 "not1_implies_pSuc";

 "pSuc_is_plus_one";

 "sum_Rep_pnat";

 "sum_Rep_pnat_sum";

 "pnat_add_assoc";

 "pnat_add_left_commute";

 "pnat_add_left_cancel";

 "pnat_add_right_cancel";

 "pnat_no_add_ident";

 "pnat_less_not_refl";

 "pnat_less_not_refl2";

 "Rep_pnat_not_less0";

 "Rep_pnat_not_less_one";

 "Rep_pnat_gt_implies_not0";

 "pnat_less_linear";

 "Rep_pnat_le_one";

 "lemma_less_ex_sum_Rep_pnat";

 "pnat_le_iff_Rep_pnat_le";

 "pnat_add_left_cancel_le";

 "pnat_add_left_cancel_less";

 "pnat_add_lessD1";

 "pnat_not_add_less1";

 "pnat_not_add_less2";

PNat.ML:qed_spec_mp 

 "pnat_add_leD1";

 "pnat_add_leD2";

PNat.ML:qed 

 "pnat_less_add_eq_less";

 "pnat_less_iff";

 "pnat_linear_Ex_eq";

 "pnat_eq_lessI";

 "Rep_pnat_mult_1";

 "Rep_pnat_mult_1_right";

 "mult_Rep_pnat";

 "mult_Rep_pnat_mult";

 "pnat_mult_commute";           "(?m::pnat) * (?n::pnat) = ?n * ?m"

 "pnat_add_mult_distrib";

 "pnat_add_mult_distrib2";

 "pnat_mult_assoc";

 "pnat_mult_left_commute";

 "pnat_mult_1";

 "pnat_mult_1_left";

 "pnat_mult_less_mono2";

 "pnat_mult_less_mono1";

 "pnat_mult_less_cancel2";

 "pnat_mult_less_cancel1";

 "pnat_mult_cancel2";

 "pnat_mult_cancel1";

 "pnat_same_multI2";

 "eq_Abs_pnat";

 "pnat_one_iff";

 "pnat_two_eq";

 "inj_pnat_of_nat";

 "nat_add_one_less";

 "nat_add_one_less1";

 "pnat_of_nat_add";

 "pnat_of_nat_less_iff";

 "pnat_of_nat_mult";

PRat.ML:qed ------------------------------------------------------------------

 "prat_trans_lemma";

   	  "[| (?x1.0::pnat) * (?y2.0::pnat) = (?x2.0::pnat) * (?y1.0::pnat);

   	      ?x2.0 * (?y3.0::pnat) = (?x3.0::pnat) * ?y2.0 |]

   	   ==> ?x1.0 * ?y3.0 = ?x3.0 * ?y1.0"

 "ratrel_iff";

 "ratrelI";

 "ratrelE_lemma";

 "ratrelE";

 "ratrel_refl";

 "equiv_ratrel";

 "ratrel_in_prat";

 "inj_on_Abs_prat";

 "inj_Rep_prat";

 "inj_prat_of_pnat";

 "eq_Abs_prat";

 "qinv_congruent";

 "qinv";

 "qinv_qinv";

 "inj_qinv";

 "qinv_1";

 "prat_add_congruent2_lemma";

 "prat_add_congruent2";

 "prat_add";

 "prat_add_commute";

 "prat_add_assoc";

 "prat_add_left_commute";

 "pnat_mult_congruent2";

 "prat_mult";

 "prat_mult_commute";

 "prat_mult_assoc";

 "prat_mult_left_commute";

 "prat_mult_1";

 "prat_mult_1_right";

 "prat_of_pnat_add";

 "prat_of_pnat_mult";

 "prat_mult_qinv";

 "prat_mult_qinv_right";

 "prat_qinv_ex";

 "prat_qinv_ex1";

 "prat_qinv_left_ex1";

 "prat_mult_inv_qinv";

 "prat_as_inverse_ex";

 "qinv_mult_eq";

 "prat_add_mult_distrib";

 "prat_add_mult_distrib2";

 "prat_less_iff";

 "prat_lessI";

 "prat_lessE_lemma";

 "prat_lessE";

 "prat_less_trans";

 "prat_less_not_refl";

 "prat_less_not_sym";

 "lemma_prat_dense";

 "prat_lemma_dense";

 "prat_dense";

 "prat_add_less2_mono1";

 "prat_add_less2_mono2";

 "prat_mult_less2_mono1";

 "prat_mult_left_less2_mono1";

 "lemma_prat_add_mult_mono";

 "qless_Ex";

 "lemma_prat_less_linear";

 "prat_linear";

 "prat_linear_less2";

 "lemma1_qinv_prat_less";

 "lemma2_qinv_prat_less";

 "qinv_prat_less";

 "prat_qinv_gt_1";

 "prat_qinv_is_gt_1";

 "prat_less_1_2";

 "prat_less_qinv_2_1";

 "prat_mult_qinv_less_1";

 "prat_self_less_add_self";

 "prat_self_less_add_right";

 "prat_self_less_add_left";

 "prat_self_less_mult_right";

 "prat_leI";

 "prat_leD";

 "prat_less_le_iff";

 "not_prat_leE";

 "prat_less_imp_le";

 "prat_le_imp_less_or_eq";

 "prat_less_or_eq_imp_le";

 "prat_le_eq_less_or_eq";

 "prat_le_refl";

 "prat_le_less_trans";

 "prat_le_trans";

 "not_less_not_eq_prat_less";

 "prat_add_less_mono";

 "prat_mult_less_mono";

 "prat_mult_left_le2_mono1";

 "prat_mult_le2_mono1";

 "qinv_prat_le";

 "prat_add_left_le2_mono1";

 "prat_add_le2_mono1";

 "prat_add_le_mono";

 "prat_add_right_less_cancel";

 "prat_add_left_less_cancel";

 "Abs_prat_mult_qinv";

 "lemma_Abs_prat_le1";

 "lemma_Abs_prat_le2";

 "lemma_Abs_prat_le3";

 "pre_lemma_gleason9_34";

 "pre_lemma_gleason9_34b";

 "prat_of_pnat_less_iff";

 "lemma_prat_less_1_memEx";

 "lemma_prat_less_1_set_non_empty";

 "empty_set_psubset_lemma_prat_less_1_set";

 "lemma_prat_less_1_not_memEx";

 "lemma_prat_less_1_set_not_rat_set";

 "lemma_prat_less_1_set_psubset_rat_set";

 "preal_1";

       "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))}

     	: {A::prat set.

     	   {} < A &

     	   A < UNIV &

     	   (ALL y::prat:A. (ALL z::prat. z < y --> z : A) & Bex A (op < y))}"

PReal.ML:qed -----------------------------------------------------------------

 "inj_on_Abs_preal";           "inj_on Abs_preal preal"

 "inj_Rep_preal";

 "empty_not_mem_preal";

 "one_set_mem_preal";

 "preal_psubset_empty";

 "Rep_preal_psubset_empty";

 "mem_Rep_preal_Ex";

 "prealI1";                    

      "[| {} < (?A::prat set); ?A < UNIV;

    	  ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |]

       ==> ?A : preal"

 "prealI2";

 "prealE_lemma";

 "prealE_lemma1";

 "prealE_lemma2";

 "prealE_lemma3";

 "prealE_lemma3a";

 "prealE_lemma3b";

 "prealE_lemma4";

 "prealE_lemma4a";

 "not_mem_Rep_preal_Ex";

 "lemma_prat_less_set_mem_preal";

 "lemma_prat_set_eq";

 "inj_preal_of_prat";

 "not_in_preal_ub";

 "preal_less_not_refl";

 "preal_not_refl2";

 "preal_less_trans";

 "preal_less_not_sym";

 "preal_linear";

              "(?r1.0::preal) < (?r2.0::preal) | ?r1.0 = ?r2.0 | ?r2.0 < ?r1.0"

 "preal_linear_less2";

 "preal_add_commute";          "(?x::preal) + (?y::preal) = ?y + ?x"

 "preal_add_set_not_empty";

 "preal_not_mem_add_set_Ex";

 "preal_add_set_not_prat_set";

 "preal_add_set_lemma3";

 "preal_add_set_lemma4";

 "preal_mem_add_set";

 "preal_add_assoc";            

 "preal_add_left_commute";

 "preal_mult_commute";          "(?x::preal) * (?y::preal) = ?y * ?x"

 "preal_mult_set_not_empty";

 "preal_not_mem_mult_set_Ex";

 "preal_mult_set_not_prat_set";

 "preal_mult_set_lemma3";

 "preal_mult_set_lemma4";

 "preal_mem_mult_set";

 "preal_mult_assoc";

 "preal_mult_left_commute";

 "preal_mult_1";

 "preal_mult_1_right";

 "preal_add_assoc_cong";

 "preal_add_assoc_swap";

 "mem_Rep_preal_addD";

 "mem_Rep_preal_addI";

 "mem_Rep_preal_add_iff";

 "mem_Rep_preal_multD";

 "mem_Rep_preal_multI";

 "mem_Rep_preal_mult_iff";

 "lemma_add_mult_mem_Rep_preal";

 "lemma_add_mult_mem_Rep_preal1";

 "lemma_preal_add_mult_distrib";

 "lemma_preal_add_mult_distrib2";

 "preal_add_mult_distrib2";

 "preal_add_mult_distrib";

 "qinv_not_mem_Rep_preal_Ex";

 "lemma_preal_mem_inv_set_ex";

 "preal_inv_set_not_empty";

 "qinv_mem_Rep_preal_Ex";

 "preal_not_mem_inv_set_Ex";

 "preal_inv_set_not_prat_set";

 "preal_inv_set_lemma3";

 "preal_inv_set_lemma4";

 "preal_mem_inv_set";

 "preal_mem_mult_invD";

 "lemma1_gleason9_34";

 "lemma1b_gleason9_34";

 "lemma_gleason9_34a";

 "lemma_gleason9_34";

 "lemma1_gleason9_36";

 "lemma2_gleason9_36";

 "lemma_gleason9_36";

 "lemma_gleason9_36a";

 "preal_mem_mult_invI";

 "preal_mult_inv";

 "preal_mult_inv_right";

 "eq_Abs_preal";

 "Rep_preal_self_subset";

 "Rep_preal_sum_not_subset";

 "Rep_preal_sum_not_eq";

 "preal_self_less_add_left";

 "preal_self_less_add_right";

 "preal_leD";

 "not_preal_leE";

 "preal_leI";

 "preal_less_le_iff";

 "preal_less_imp_le";

 "preal_le_imp_less_or_eq";

 "preal_less_or_eq_imp_le";

 "preal_le_refl";

 "preal_le_trans";

 "preal_le_anti_sym";

 "preal_neq_iff";

 "preal_less_le";

 "lemma_psubset_mem";

 "lemma_psubset_not_refl";

 "psubset_trans";

 "subset_psubset_trans";

 "subset_psubset_trans2";

 "psubsetD";

 "lemma_ex_mem_less_left_add1";

 "preal_less_set_not_empty";

 "lemma_ex_not_mem_less_left_add1";

 "preal_less_set_not_prat_set";

 "preal_less_set_lemma3";

 "preal_less_set_lemma4";

 "preal_mem_less_set";

 "preal_less_add_left_subsetI";

 "lemma_sum_mem_Rep_preal_ex";

 "preal_less_add_left_subsetI2";

 "preal_less_add_left";

 "preal_less_add_left_Ex";        

 "preal_add_less2_mono1";

 "preal_add_less2_mono2";

 "preal_mult_less_mono1";

 "preal_mult_left_less_mono1";

 "preal_mult_left_le_mono1";

 "preal_mult_le_mono1";

 "preal_add_left_le_mono1";

 "preal_add_le_mono1";

 "preal_add_right_less_cancel";

 "preal_add_left_less_cancel";

 "preal_add_less_iff1";

 "preal_add_less_iff2";

 "preal_add_less_mono";

 "preal_mult_less_mono";

 "preal_add_right_cancel";

 "preal_add_left_cancel";

 "preal_add_left_cancel_iff";

 "preal_add_right_cancel_iff";

 "preal_sup_mem_Ex";

 "preal_sup_set_not_empty";

 "preal_sup_not_mem_Ex";

 "preal_sup_not_mem_Ex1";

 "preal_sup_set_not_prat_set";

 "preal_sup_set_not_prat_set1";

 "preal_sup_set_lemma3";

 "preal_sup_set_lemma3_1";

 "preal_sup_set_lemma4";

 "preal_sup_set_lemma4_1";

 "preal_sup";

 "preal_sup1";

 "preal_psup_leI";

 "preal_psup_leI2";

 "preal_psup_leI2b";

 "preal_psup_leI2a";

 "psup_le_ub";

 "psup_le_ub1";

 "preal_complete";

 "lemma_preal_rat_less";

 "lemma_preal_rat_less2";

 "preal_of_prat_add";

 "lemma_preal_rat_less3";

 "lemma_preal_rat_less4";

 "preal_of_prat_mult";

 "preal_of_prat_less_iff"; "(preal_of_prat ?p < preal_of_prat ?q) = (?p < ?q)"

RealDef.ML:qed ---------------------------------------------------------------

 "preal_trans_lemma";      

 "realrel_iff";		   

 "realrelI";		   

   "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel"

 "realrelE_lemma";	   

 "realrelE";		   

 "realrel_refl";	   

 "equiv_realrel";	   

 "realrel_in_real";	   

 "inj_on_Abs_REAL";	   

 "inj_Rep_REAL";	   

 "inj_real_of_preal";	   

 "eq_Abs_REAL";		   

 "real_minus_congruent";   

 "real_minus";		   

        "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})"

 "real_minus_minus";	   (**)"- (- (?z::real)) = ?z"

 "inj_real_minus";	   "inj uminus"

 "real_minus_zero";	   (**)"- 0 = 0"

 "real_minus_zero_iff";	   (**)"(- ?x = 0) = (?x = 0)"

 "real_add_congruent2";    

    "congruent2 realrel

     (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)"

 "real_add";

       "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) +

     	Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =

     	Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})"

 "real_add_commute";	   (**)"(?z::real) + (?w::real) = ?w + ?z"

 "real_add_assoc";	   (**)

 "real_add_left_commute";  (**)

 "real_add_zero_left";	   (**)"0 + ?z = ?z"

 "real_add_zero_right";	   (**)

 "real_add_minus";	   (**)"?z + - ?z = 0"

 "real_add_minus_left";	   (**)

 "real_add_minus_cancel";  (**)"?z + (- ?z + ?w) = ?w"

 "real_minus_add_cancel";  (**)"- ?z + (?z + ?w) = ?w"

 "real_minus_ex";	   "EX y. ?x + y = 0"

 "real_minus_ex1";	   

 "real_minus_left_ex1";	   "EX! y. y + ?x = 0"

 "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"

 "real_as_add_inverse_ex"; "EX y. ?x = - y"

 "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y"

 "real_add_left_cancel";   "(?x + ?y = ?x + ?z) = (?y = ?z)"

 "real_add_right_cancel";  "(?y + ?x = ?z + ?x) = (?y = ?z)"

 "real_diff_0";		   (**)"0 - ?x = - ?x"

 "real_diff_0_right";	   (**)"?x - 0 = ?x"

 "real_diff_self";         (**)"?x - ?x = 0"

 "real_mult_congruent2_lemma";

 "real_mult_congruent2";

     "congruent2 realrel

       (%p1 p2.

   	   (%(x1, y1).

   	       (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)})

   		p2) p1)"

 "real_mult";		    

  	 "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) *

  	  Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =

  	  Abs_REAL

  	   (realrel ``

  	    {(?x1.0 * ?x2.0 + ?y1.0 * ?y2.0, ?x1.0 * ?y2.0 + ?x2.0 * ?y1.0)})"

 "real_mult_commute";	   (**)"?z * ?w = ?w * ?z"

 "real_mult_assoc";	   (**)

 "real_mult_left_commute";  

                       (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"

 "real_mult_1";		   (**)"1 * ?z = ?z"

 "real_mult_1_right";	   (**)"?z * 1 = ?z"

 "real_mult_0";		   (**)

 "real_mult_0_right";	   (**)"?z * 0 = 0"

 "real_mult_minus_eq1";	   (**)"- ?x * ?y = - (?x * ?y)"

 "real_mult_minus_eq2";	   (**)"?x * - ?y = - (?x * ?y)"

 "real_mult_minus_1";	   (**)"- 1 * ?z = - ?z"

 "real_mult_minus_1_right";(**)"?z * - 1 = - ?z"

 "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y"

 "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y"

 "real_add_assoc_cong";	

                    "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)"

 "real_add_assoc_swap";	   (**)"?z + (?v + ?w) = ?v + (?z + ?w)"

 "real_add_mult_distrib";  (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"

 "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"

 "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"

 "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"

 "real_zero_not_eq_one";    

 "real_zero_iff";	    "0 = Abs_REAL (realrel `` {(?x, ?x)})"

 "real_mult_inv_right_ex";  "?x ~= 0 ==> EX y. ?x * y = 1"

 "real_mult_inv_left_ex";   "?x ~= 0 ==> inverse ?x * ?x = 1"

 "real_mult_inv_left";	    

 "real_mult_inv_right";     "?x ~= 0 ==> ?x * inverse ?x = 1"

 "INVERSE_ZERO";            "inverse 0 = 0"

 "DIVISION_BY_ZERO";  (*NOT for adding to default simpset*)"?a / 0 = 0"

 "real_mult_left_cancel";   (**)"?c ~= 0 ==> (?c * ?a = ?c * ?b) = (?a = ?b)"

 "real_mult_right_cancel";  (**)"?c ~= 0 ==> (?a * ?c = ?b * ?c) = (?a = ?b)"

 "real_mult_left_cancel_ccontr";  "?c * ?a ~= ?c * ?b ==> ?a ~= ?b"

 "real_mult_right_cancel_ccontr"; "?a * ?c ~= ?b * ?c ==> ?a ~= ?b"

 "real_inverse_not_zero";   "?x ~= 0 ==> inverse ?x ~= 0"

 "real_mult_not_zero";	    "[| ?x ~= 0; ?y ~= 0 |] ==> ?x * ?y ~= 0"

 "real_inverse_inverse";    "inverse (inverse ?x) = ?x"

 "real_inverse_1";	    "inverse 1 = 1"

 "real_minus_inverse";	    "inverse (- ?x) = - inverse ?x"

 "real_inverse_distrib";    "inverse (?x * ?y) = inverse ?x * inverse ?y"

 "real_times_divide1_eq";   (**)"?x * (?y / ?z) = ?x * ?y / ?z"

 "real_times_divide2_eq";   (**)"?y / ?z * ?x = ?y * ?x / ?z"

 "real_divide_divide1_eq";  (**)"?x / (?y / ?z) = ?x * ?z / ?y"

 "real_divide_divide2_eq";  (**)"?x / ?y / ?z = ?x / (?y * ?z)"

 "real_minus_divide_eq";    (**)"- ?x / ?y = - (?x / ?y)"

 "real_divide_minus_eq";    (**)"?x / - ?y = - (?x / ?y)"

 "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"

 "preal_lemma_eq_rev_sum";

                     "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y"

 "preal_add_left_commute_cancel";

            "?x + (?b + ?y) = ?x1.0 + (?b + ?y1.0) ==> ?x + ?y = ?x1.0 + ?y1.0"

 "preal_lemma_for_not_refl"; 

 "real_less_not_refl";	     "~ ?R < ?R"  

 "real_not_refl2";	     

 "preal_lemma_trans";	     

 "real_less_trans";	     

 "real_less_not_sym";	     

 "real_of_preal_add";	  

    "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0"

 "real_of_preal_mult";	     

 "real_of_preal_ExI";	     

 "real_of_preal_ExD";	     

 "real_of_preal_iff";	     

 "real_of_preal_trichotomy"; 

 "real_of_preal_trichotomyE";

 "real_of_preal_lessD";	     

 "real_of_preal_lessI";	     

                  "?m1.0 < ?m2.0 ==> real_of_preal ?m1.0 < real_of_preal ?m2.0"

 "real_of_preal_less_iff1";  

 "real_of_preal_minus_less_self";

 "real_of_preal_minus_less_zero";

 "real_of_preal_not_minus_gt_zero";

 "real_of_preal_zero_less";

 "real_of_preal_not_less_zero";

 "real_minus_minus_zero_less";

 "real_of_preal_sum_zero_less";

 "real_of_preal_minus_less_all";

 "real_of_preal_not_minus_gt_all";

 "real_of_preal_minus_less_rev1";

 "real_of_preal_minus_less_rev2";

 "real_of_preal_minus_less_rev_iff";

 "real_linear";            "?R1.0 < ?R2.0 | ?R1.0 = ?R2.0 | ?R2.0 < ?R1.0"

 "real_neq_iff";	   

 "real_linear_less2";	

       "[| ?R1.0 < ?R2.0 ==> ?P; ?R1.0 = ?R2.0 ==> ?P; ?R2.0 < ?R1.0 ==> ?P |]

								     ==> ?P"

 "real_leI";		   

 "real_leD";		   "~ ?w < ?z ==> ?z <= ?w"

 "real_less_le_iff";	   

 "not_real_leE";	   

 "real_le_imp_less_or_eq"; 

 "real_less_or_eq_imp_le"; 

 "real_le_less";	   

 "real_le_refl";	   "?w <= ?w"

 "real_le_linear";	   

 "real_le_trans";	   "[| ?i <= ?j; ?j <= ?k |] ==> ?i <= ?k"

 "real_le_anti_sym";       "[| ?z <= ?w; ?w <= ?z |] ==> ?z = ?w"

 "not_less_not_eq_real_less";

 "real_less_le";           "(?w < ?z) = (?w <= ?z & ?w ~= ?z)"

 "real_minus_zero_less_iff";

 "real_minus_zero_less_iff2";

 "real_less_add_positive_left_Ex";

 "real_less_sum_gt_zero";  "?W < ?S ==> 0 < ?S + - ?W"

 "real_lemma_change_eq_subj";

 "real_sum_gt_zero_less";  "0 < ?S + - ?W ==> ?W < ?S"

 "real_less_sum_gt_0_iff"; "(0 < ?S + - ?W) = (?W < ?S)"

 "real_less_eq_diff";	   "(?x < ?y) = (?x - ?y < 0)"

 "real_add_diff_eq";	   (**)"?x + (?y - ?z) = ?x + ?y - ?z"

 "real_diff_add_eq";	   (**)"?x - ?y + ?z = ?x + ?z - ?y"

 "real_diff_diff_eq";	   (**)"?x - ?y - ?z = ?x - (?y + ?z)"

 "real_diff_diff_eq2";	   (**)"?x - (?y - ?z) = ?x + ?z - ?y"

 "real_diff_less_eq";	   "(?x - ?y < ?z) = (?x < ?z + ?y)"

 "real_less_diff_eq";	   

 "real_diff_le_eq";	   "(?x - ?y <= ?z) = (?x <= ?z + ?y)"

 "real_le_diff_eq";	   

 "real_diff_eq_eq";	   (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"

 "real_eq_diff_eq";	   (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"

 "real_less_eqI";	   

 "real_le_eqI";		   

 "real_eq_eqI";            "?x - ?y = ?x' - ?y' ==> (?x = ?y) = (?x' = ?y')"

RealOrd.ML:qed ---------------------------------------------------------------

 "real_add_cancel_21";     "(?x + (?y + ?z) = ?y + ?u) = (?x + ?z = ?u)"

 "real_add_cancel_end";    "(?x + (?y + ?z) = ?y) = (?x = - ?z)"

 "real_minus_diff_eq";     (*??*)"- (?x - ?y) = ?y - ?x"

 "real_gt_zero_preal_Ex";

 "real_gt_preal_preal_Ex";

 "real_ge_preal_preal_Ex";

 "real_less_all_preal";    "?y <= 0 ==> ALL x. ?y < real_of_preal x"

 "real_less_all_real2";

 "real_lemma_add_positive_imp_less";

 "real_ex_add_positive_left_less";"EX T. 0 < T & ?R + T = ?S ==> ?R < ?S"

 "real_less_iff_add";

 "real_of_preal_le_iff";

 "real_mult_order";        "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x * ?y"

 "neg_real_mult_order";

 "real_mult_less_0";       "[| 0 < ?x; ?y < 0 |] ==> ?x * ?y < 0"

 "real_zero_less_one";     "0 < 1"

 "real_add_right_cancel_less";       "(?v + ?z < ?w + ?z) = (?v < ?w)"

 "real_add_left_cancel_less";

 "real_add_right_cancel_le";

 "real_add_left_cancel_le";

 "real_add_less_le_mono";  "[| ?w' < ?w; ?z' <= ?z |] ==> ?w' + ?z' < ?w + ?z"

 "real_add_le_less_mono";  "[| ?w' <= ?w; ?z' < ?z |] ==> ?w' + ?z' < ?w + ?z"

 "real_add_less_mono2";

 "real_less_add_right_cancel";

 "real_less_add_left_cancel";                  "?C + ?A < ?C + ?B ==> ?A < ?B"

 "real_le_add_right_cancel";

 "real_le_add_left_cancel";                  "?C + ?A <= ?C + ?B ==> ?A <= ?B"

 "real_add_order";                      "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x + ?y"

 "real_le_add_order";

 "real_add_less_mono";

 "real_add_left_le_mono1";

 "real_add_le_mono";

 "real_less_Ex";

 "real_add_minus_positive_less_self";  "0 < ?r ==> ?u + - ?r < ?u"

 "real_le_minus_iff";      "(- ?s <= - ?r) = (?r <= ?s)"

 "real_le_square";

 "real_of_posnat_one";

 "real_of_posnat_two";

 "real_of_posnat_add";     "real_of_posnat ?n1.0 + real_of_posnat ?n2.0 =

                            real_of_posnat (?n1.0 + ?n2.0) + 1"

 "real_of_posnat_add_one";   

 "real_of_posnat_Suc";	     

 "inj_real_of_posnat";	     

 "real_of_nat_zero";	     

 "real_of_nat_one";	    "real (Suc 0) = 1"

 "real_of_nat_add";	     

 "real_of_nat_Suc";	     

 "real_of_nat_less_iff";     

 "real_of_nat_le_iff";	     

 "inj_real_of_nat";	     

 "real_of_nat_ge_zero";	     

 "real_of_nat_mult";	     

 "real_of_nat_inject";	     

RealOrd.ML:qed_spec_mp 	     

 "real_of_nat_diff";	     

RealOrd.ML:qed 		     

 "real_of_nat_zero_iff";     

 "real_of_nat_neg_int";	     

 "real_inverse_gt_0";	     

 "real_inverse_less_0";	     

 "real_mult_less_mono1";     

 "real_mult_less_mono2";     

 "real_mult_less_cancel1";   

                  "(?k * ?m < ?k * ?n) = (0 < ?k & ?m < ?n | ?k < 0 & ?n < ?m)"

 "real_mult_less_cancel2";   

 "real_mult_less_iff1";	     

 "real_mult_less_iff2";	     

 "real_mult_le_cancel_iff1";  

 "real_mult_le_cancel_iff2"; 

 "real_mult_le_less_mono1";  

 "real_mult_less_mono";	     

 "real_mult_less_mono'";     

 "real_gt_zero";	     "1 <= ?x ==> 0 < ?x"

 "real_mult_self_le";	     "[| 1 < ?r; 1 <= ?x |] ==> ?x <= ?r * ?x"

 "real_mult_self_le2";	     

 "real_inverse_less_swap";   

 "real_mult_is_0";	     

 "real_inverse_add";	     

 "real_minus_zero_le_iff";   

 "real_minus_zero_le_iff2";  

 "real_sum_squares_cancel";  "?x * ?x + ?y * ?y = 0 ==> ?x = 0"

 "real_sum_squares_cancel2"; "?x * ?x + ?y * ?y = 0 ==> ?y = 0"

 "real_0_less_mult_iff";     

 "real_0_le_mult_iff";	     

 "real_mult_less_0_iff";  "(?x * ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"

 "real_mult_le_0_iff";       

RealInt.ML:qed --------------------------------------------------------------- 

 "real_of_int_congruent";   

 "real_of_int";           "real (Abs_Integ (intrel `` {(?i, ?j)})) =

                           Abs_REAL

                            (realrel ``

                             {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)),

                              preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})"

 "inj_real_of_int";	    

 "real_of_int_zero";	    

 "real_of_one";		    

 "real_of_int_add";	    "real ?x + real ?y = real (?x + ?y)"

 "real_of_int_minus";	    

 "real_of_int_diff";	    

 "real_of_int_mult";	    "real ?x * real ?y = real (?x * ?y)"

 "real_of_int_Suc";	    

 "real_of_int_real_of_nat"; 

 "real_of_nat_real_of_int"; 

 "real_of_int_zero_cancel"; 

 "real_of_int_less_cancel"; 

 "real_of_int_inject";	    

 "real_of_int_less_mono";   

 "real_of_int_less_iff";    

 "real_of_int_le_iff";      

RealBin.ML:qed ---------------------------------------------------------------

 "real_number_of";          "real (number_of ?w) = number_of ?w"

 "real_numeral_0_eq_0";	     

 "real_numeral_1_eq_1";	     

 "add_real_number_of";	     

 "minus_real_number_of";     

 "diff_real_number_of";	     

 "mult_real_number_of";	     

 "real_mult_2";		    (**)"2 * ?z = ?z + ?z"

 "real_mult_2_right";       (**)"?z * 2 = ?z + ?z"

 "eq_real_number_of";	     

 "less_real_number_of";	     

 "le_real_number_of_eq_not_less"; 

 "real_minus_1_eq_m1";      "- 1 = -1"(*uminus.. = "-.."*)

 "real_mult_minus1";        (**)"-1 * ?z = - ?z"

 "real_mult_minus1_right";  (**)"?z * -1 = - ?z"

 "zero_less_real_of_nat_iff";"(0 < real ?n) = (0 < ?n)"

 "zero_le_real_of_nat_iff";

 "real_add_number_of_left";

 "real_mult_number_of_left";

         "number_of ?v * (number_of ?w * ?z) = number_of (bin_mult ?v ?w) * ?z"

 "real_add_number_of_diff1";

 "real_add_number_of_diff2";"number_of ?v + (?c - number_of ?w) =

                             number_of (bin_add ?v (bin_minus ?w)) + ?c"

 "real_of_nat_number_of";

       "real (number_of ?v) = (if neg (number_of ?v) then 0 else number_of ?v)"

 "real_less_iff_diff_less_0"; "(?x < ?y) = (?x - ?y < 0)"

 "real_eq_iff_diff_eq_0";

 "real_le_iff_diff_le_0";

 "left_real_add_mult_distrib";

                           (**)"?i * ?u + (?j * ?u + ?k) = (?i + ?j) * ?u + ?k"

 "real_eq_add_iff1";

                   "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)"

 "real_eq_add_iff2";

 "real_less_add_iff1";

 "real_less_add_iff2";

 "real_le_add_iff1";

 "real_le_add_iff2";

 "real_mult_le_mono1";

 "real_mult_le_mono2";

 "real_mult_le_mono";

            "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l"

RealArith0.ML:qed ------------------------------------------------------------

 "real_diff_minus_eq";       (**)"?x - - ?y = ?x + ?y"

 "real_0_divide";            (**)"0 / ?x = 0"

 "real_0_less_inverse_iff";  "(0 < inverse ?x) = (0 < ?x)"

 "real_inverse_less_0_iff";

 "real_0_le_inverse_iff";

 "real_inverse_le_0_iff";

 "REAL_DIVIDE_ZERO";         "?x / 0 = 0"(*!!!*)

 "real_inverse_eq_divide";

 "real_0_less_divide_iff";"(0 < ?x / ?y) = (0 < ?x & 0 < ?y | ?x < 0 & ?y < 0)"

 "real_divide_less_0_iff";"(?x / ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"

 "real_0_le_divide_iff";

 "real_divide_le_0_iff";

                 "(?x / ?y <= 0) = ((?x <= 0 | ?y <= 0) & (0 <= ?x | 0 <= ?y))"

 "real_inverse_zero_iff";

 "real_divide_eq_0_iff";     "(?x / ?y = 0) = (?x = 0 | ?y = 0)"(*!!!*)

 "real_divide_self_eq";      "?h ~= 0 ==> ?h / ?h = 1"(**)

 "real_minus_less_minus";    "(- ?y < - ?x) = (?x < ?y)"

 "real_mult_less_mono1_neg"; "[| ?i < ?j; ?k < 0 |] ==> ?j * ?k < ?i * ?k"

 "real_mult_less_mono2_neg"; 

 "real_mult_le_mono1_neg";   

 "real_mult_le_mono2_neg";   

 "real_mult_less_cancel2";   

 "real_mult_le_cancel2";     

 "real_mult_less_cancel1";   

 "real_mult_le_cancel1";     

 "real_mult_eq_cancel1";     "(?k * ?m = ?k * ?n) = (?k = 0 | ?m = ?n)"

 "real_mult_eq_cancel2";     "(?m * ?k = ?n * ?k) = (?k = 0 | ?m = ?n)"

 "real_mult_div_cancel1";    (**)"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"

 "real_mult_div_cancel_disj";

                        "?k * ?m / (?k * ?n) = (if ?k = 0 then 0 else ?m / ?n)"

 "pos_real_le_divide_eq";    

 "neg_real_le_divide_eq";    

 "pos_real_divide_le_eq";    

 "neg_real_divide_le_eq";    

 "pos_real_less_divide_eq";  

 "neg_real_less_divide_eq";  

 "pos_real_divide_less_eq";  

 "neg_real_divide_less_eq";  

 "real_eq_divide_eq";        (**)"?z ~= 0 ==> (?x = ?y / ?z) = (?x * ?z = ?y)"

 "real_divide_eq_eq";	     (**)"?z ~= 0 ==> (?y / ?z = ?x) = (?y = ?x * ?z)"

 "real_divide_eq_cancel2";   "(?m / ?k = ?n / ?k) = (?k = 0 | ?m = ?n)"

 "real_divide_eq_cancel1";   "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)"

 "real_inverse_less_iff";    

 "real_inverse_le_iff";	     

 "real_divide_1";            (**)"?x / 1 = ?x"

 "real_divide_minus1";	     (**)"?x / -1 = - ?x"

 "real_minus1_divide";	     (**)"-1 / ?x = - (1 / ?x)"

 "real_lbound_gt_zero";

           "[| 0 < ?d1.0; 0 < ?d2.0 |] ==> EX e. 0 < e & e < ?d1.0 & e < ?d2.0"

 "real_inverse_eq_iff";	     "(inverse ?x = inverse ?y) = (?x = ?y)"

 "real_divide_eq_iff";	     "(?z / ?x = ?z / ?y) = (?z = 0 | ?x = ?y)"

 "real_less_minus"; 	     "(?x < - ?y) = (?y < - ?x)"

 "real_minus_less"; 	     "(- ?x < ?y) = (- ?y < ?x)"

 "real_le_minus"; 	     

 "real_minus_le";            "(- ?x <= ?y) = (- ?y <= ?x)"

 "real_equation_minus";	     (**)"(?x = - ?y) = (?y = - ?x)"

 "real_minus_equation";	     (**)"(- ?x = ?y) = (- ?y = ?x)"

 "real_add_minus_iff";	     (**)"(?x + - ?a = 0) = (?x = ?a)"

 "real_minus_eq_cancel";     (**)"(- ?b = - ?a) = (?b = ?a)"

 "real_add_eq_0_iff";	     (**)"(?x + ?y = 0) = (?y = - ?x)"

 "real_add_less_0_iff";	     "(?x + ?y < 0) = (?y < - ?x)"

 "real_0_less_add_iff";	     

 "real_add_le_0_iff";	     

 "real_0_le_add_iff";	     

 "real_0_less_diff_iff";     "(0 < ?x - ?y) = (?y < ?x)"

 "real_0_le_diff_iff";	     

 "real_minus_diff_eq";	     (**)"- (?x - ?y) = ?y - ?x"

 "real_less_half_sum";	     "?x < ?y ==> ?x < (?x + ?y) / 2"

 "real_gt_half_sum";	     

 "real_dense";               "?x < ?y ==> EX r. ?x < r & r < ?y"

RealArith ///!!!///-----------------------------------------------------------

RComplete.ML:qed -------------------------------------------------------------

 "real_sum_of_halves";       (**)"?x / 2 + ?x / 2 = ?x"

 "real_sup_lemma1";

 "real_sup_lemma2";

 "posreal_complete";

 "real_isLub_unique";

 "real_order_restrict";

 "posreals_complete";

 "real_sup_lemma3";

 "lemma_le_swap2";

 "lemma_real_complete2b";

 "reals_complete";

 "real_of_nat_Suc_gt_zero";

 "reals_Archimedean";     "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x"

 "reals_Archimedean2";

RealAbs.ML:qed 

 "abs_nat_number_of";

      "abs (number_of ?v) =

       (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)"

 "abs_split";

 "abs_iff";

 "abs_zero";              "abs 0 = 0"

 "abs_one";

 "abs_eqI1";

 "abs_eqI2";

 "abs_minus_eqI2";

 "abs_minus_eqI1";

 "abs_ge_zero";           "0 <= abs ?x"

 "abs_idempotent";        "abs (abs ?x) = abs ?x"

 "abs_zero_iff";          "(abs ?x = 0) = (?x = 0)"

 "abs_ge_self";           "?x <= abs ?x"

 "abs_ge_minus_self";

 "abs_mult";              "abs (?x * ?y) = abs ?x * abs ?y"

 "abs_inverse";           "abs (inverse ?x) = inverse (abs ?x)"

 "abs_mult_inverse";

 "abs_triangle_ineq";     "abs (?x + ?y) <= abs ?x + abs ?y"

 "abs_triangle_ineq_four";

 "abs_minus_cancel";

 "abs_minus_add_cancel";

 "abs_triangle_minus_ineq";

RealAbs.ML:qed_spec_mp 

 "abs_add_less";   "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s"

RealAbs.ML:qed 

 "abs_add_minus_less";

 "real_mult_0_less";       "(0 * ?x < ?r) = (0 < ?r)"

 "real_mult_less_trans";

 "real_mult_le_less_trans";

 "abs_mult_less";

 "abs_mult_less2";

 "abs_less_gt_zero";

 "abs_minus_one";         "abs -1 = 1"

 "abs_disj";              "abs ?x = ?x | abs ?x = - ?x"

 "abs_interval_iff";

 "abs_le_interval_iff";

 "abs_add_pos_gt_zero";

 "abs_add_one_gt_zero";

 "abs_not_less_zero";

 "abs_circle";            "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y"

 "abs_le_zero_iff";

 "real_0_less_abs_iff";

 "abs_real_of_nat_cancel";

 "abs_add_one_not_less_self";

 "abs_triangle_ineq_three";    "abs (?w + ?x + ?y) <= abs ?w + abs ?x + abs ?y"

 "abs_diff_less_imp_gt_zero";

 "abs_diff_less_imp_gt_zero2";

 "abs_diff_less_imp_gt_zero3";

 "abs_diff_less_imp_gt_zero4";

 "abs_triangle_ineq_minus_cancel";

 "abs_sum_triangle_ineq";  

           "abs (?x + ?y + (- ?l + - ?m)) <= abs (?x + - ?l) + abs (?y + - ?m)"

RealPow.ML:qed

 "realpow_zero";           "0 ^ Suc ?n = 0"

RealPow.ML:qed_spec_mp 

 "realpow_not_zero";       "?r ~= 0 ==> ?r ^ ?n ~= 0"

 "realpow_zero_zero";      "?r ^ ?n = 0 ==> ?r = 0"

 "realpow_inverse";        "inverse (?r ^ ?n) = inverse ?r ^ ?n"

 "realpow_abs";            "abs (?r ^ ?n) = abs ?r ^ ?n"

 "realpow_add";            (**)"?r ^ (?n + ?m) = ?r ^ ?n * ?r ^ ?m"

 "realpow_one";            (**)"?r ^ 1 = ?r"

 "realpow_two";            (**)"?r ^ Suc (Suc 0) = ?r * ?r"

RealPow.ML:qed_spec_mp 

 "realpow_gt_zero";        "0 < ?r ==> 0 < ?r ^ ?n"

 "realpow_ge_zero";        "0 <= ?r ==> 0 <= ?r ^ ?n"

 "realpow_le";             "0 <= ?x & ?x <= ?y ==> ?x ^ ?n <= ?y ^ ?n"

 "realpow_less";	   

RealPow.ML:qed 		    

 "realpow_eq_one";         (**)"1 ^ ?n = 1"

 "abs_realpow_minus_one";  "abs (-1 ^ ?n) = 1"

 "realpow_mult";           (**)"(?r * ?s) ^ ?n = ?r ^ ?n * ?s ^ ?n" 

 "realpow_two_le";	   "0 <= ?r ^ Suc (Suc 0)"

 "abs_realpow_two";	   

 "realpow_two_abs";        "abs ?x ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"

 "realpow_two_gt_one";	   

RealPow.ML:qed_spec_mp 	   

 "realpow_ge_one";	   "1 < ?r ==> 1 <= ?r ^ ?n"

RealPow.ML:qed 		   

 "realpow_ge_one2";	   

 "two_realpow_ge_one";	   

 "two_realpow_gt";	   

 "realpow_minus_one";      (**)"-1 ^ (2 * ?n) = 1"  

 "realpow_minus_one_odd";  "-1 ^ Suc (2 * ?n) = - 1"

 "realpow_minus_one_even"; 

RealPow.ML:qed_spec_mp 	   

 "realpow_Suc_less";	   

 "realpow_Suc_le";         "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n"

RealPow.ML:qed 

 "realpow_zero_le";        "0 <= 0 ^ ?n"

RealPow.ML:qed_spec_mp 

 "realpow_Suc_le2";

RealPow.ML:qed 

 "realpow_Suc_le3";

RealPow.ML:qed_spec_mp 

 "realpow_less_le";        "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n"

RealPow.ML:qed 

 "realpow_le_le";      "[| 0 <= ?r; ?r < 1; ?n <= ?N |] ==> ?r ^ ?N <= ?r ^ ?n"

 "realpow_Suc_le_self";

 "realpow_Suc_less_one";

RealPow.ML:qed_spec_mp 

 "realpow_le_Suc";

 "realpow_less_Suc";

 "realpow_le_Suc2";

 "realpow_gt_ge";

 "realpow_gt_ge2";

RealPow.ML:qed 

 "realpow_ge_ge";               "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N"

 "realpow_ge_ge2";

RealPow.ML:qed_spec_mp 

 "realpow_Suc_ge_self";

 "realpow_Suc_ge_self2";

RealPow.ML:qed 

 "realpow_ge_self";

 "realpow_ge_self2";

RealPow.ML:qed_spec_mp 

 "realpow_minus_mult";          "0 < ?n ==> ?x ^ (?n - 1) * ?x = ?x ^ ?n"

 "realpow_two_mult_inverse";

                       "?r ~= 0 ==> ?r * inverse ?r ^ Suc (Suc 0) = inverse ?r"

 "realpow_two_minus";           "(- ?x) ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"

 "realpow_two_diff";

 "realpow_two_disj";

 "realpow_diff";

     "[| ?x ~= 0; ?m <= ?n |] ==> ?x ^ (?n - ?m) = ?x ^ ?n * inverse (?x ^ ?m)"

 "realpow_real_of_nat";

 "realpow_real_of_nat_two_pos"; "0 < real (Suc (Suc 0) ^ ?n)"

RealPow.ML:qed_spec_mp 

 "realpow_increasing";

 "realpow_Suc_cancel_eq";

                "[| 0 <= ?x; 0 <= ?y; ?x ^ Suc ?n = ?y ^ Suc ?n |] ==> ?x = ?y"

RealPow.ML:qed 

 "realpow_eq_0_iff";            "(?x ^ ?n = 0) = (?x = 0 & 0 < ?n)"

 "zero_less_realpow_abs_iff";

 "zero_le_realpow_abs";

 "real_of_int_power";           "real ?x ^ ?n = real (?x ^ ?n)"

 "power_real_number_of";        "number_of ?v ^ ?n = real (number_of ?v ^ ?n)"

Ring_and_Field ---///!!!///---------------------------------------------------

Complex_Numbers --///!!!///---------------------------------------------------

Real -------------///!!!///---------------------------------------------------

real_arith0.ML:qed "";

real_arith0.ML:qed "";

real_arith0.ML:qed "";

real_arith0.ML:qed "";