diff --git a/src/rational/fracScript.sml b/src/rational/fracScript.sml
index fe1d427375..64077d7de1 100644
--- a/src/rational/fracScript.sml
+++ b/src/rational/fracScript.sml
@@ -756,7 +756,7 @@ val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2. frac_sgn (frac_mul f1 f2)
         ASM_CASES_TAC ``frac_nmr f2=0i`` THEN
         ASM_CASES_TAC ``frac_nmr f2 < 0i`` THEN
         RW_TAC int_ss [INT_MUL_LZERO, INT_MUL_RZERO] THEN
-        PROVE_TAC[INT_NO_ZERODIV,INT_MUL_SIGN_CASES,INT_LT_GT,INT_LT_TOTAL] );
+        PROVE_TAC[INT_ENTIRE,INT_MUL_SIGN_CASES,INT_LT_GT,INT_LT_TOTAL] );
 
 
 (*--------------------------------------------------------------------------
@@ -782,20 +782,6 @@ val FRAC_SGN_MUL2 = store_thm("FRAC_SGN_MUL2", ``!f1 f2. frac_sgn (frac_mul f1 f
         FRAC_NMRDNM_TAC THEN
         PROVE_TAC[INT_SGN_MUL2] );
 
-(*--------------------------------------------------------------------------
- *  FRAC_SGN_MUL : thm
- *  |- !f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==>
- *      (frac_sgn (frac_mul f1 f2) = i1 * i2)
- * deleted
- *--------------------------------------------------------------------------*)
-
-(*val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==> (frac_sgn (frac_mul f1 f2) = i1 * i2)``,
-        REPEAT GEN_TAC THEN
-        REWRITE_TAC[frac_sgn_def] THEN
-        FRAC_CALC_TAC THEN
-        FRAC_NMRDNM_TAC THEN
-        PROVE_TAC[INT_SGN_MUL] );*)
-
 (*--------------------------------------------------------------------------
  *  FRAC_SGN_CASES : thm
  *  |- !f1 P.
diff --git a/src/rational/intExtensionScript.sml b/src/rational/intExtensionScript.sml
index ff5d112fa6..f06622ad5c 100644
--- a/src/rational/intExtensionScript.sml
+++ b/src/rational/intExtensionScript.sml
@@ -27,49 +27,60 @@ val _ = new_theory "intExtension";
    operations
  *--------------------------------------------------------------------------*)
 
-val SGN_def = Define `SGN x = (if x = 0i then 0i else (if x < 0i then ~1 else 1i))`;
+Definition SGN_def:
+  SGN x = if x = 0i then 0i else if x < 0i then ~1 else 1i
+End
+
+(*--------------------------------------------------------------------------
+   INT_SGN_TOTAL : thm
+   |- !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)
+ *--------------------------------------------------------------------------*)
+
+Theorem INT_SGN_TOTAL: !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)
+Proof
+  RW_TAC int_ss[SGN_def]
+QED
+
+Theorem INT_SGN_CASES:
+  !a P. (SGN a = ~1 /\ a < 0 ==> P) /\ (SGN a = 0i /\ a = 0 ==> P) /\
+        (SGN a = 1i /\ 0 < a ==> P) ==> P
+Proof
+  rw[] >> qspec_then ‘a’ strip_assume_tac INT_SGN_TOTAL >> gvs[] >>
+  gvs[SGN_def,AllCaseEqs()] >> metis_tac[INT_LT_TOTAL]
+QED
 
 (*--------------------------------------------------------------------------
    linking ABS and SGN: |- ABS x = x * SGN x, |- ABS x * SGN x = x
  *--------------------------------------------------------------------------*)
 
-val ABS_EQ_MUL_SGN = store_thm ("ABS_EQ_MUL_SGN", ``ABS x = x * SGN x``,
-  REWRITE_TAC [INT_ABS, SGN_def] THEN
-  REPEAT COND_CASES_TAC THEN
-  ASM_SIMP_TAC int_ss [GSYM INT_NEG_RMUL]) ;
+Theorem ABS_EQ_MUL_SGN: ABS x = x * SGN x
+Proof
+  rw[SGN_def, INT_ABS, GSYM INT_NEG_RMUL]
+QED
 
-val MUL_ABS_SGN = store_thm ("MUL_ABS_SGN", ``ABS x * SGN x = x``,
-  REWRITE_TAC [INT_ABS, SGN_def] THEN
-  REPEAT COND_CASES_TAC THEN
-  ASM_SIMP_TAC int_ss []) ;
+Theorem MUL_ABS_SGN: ABS x * SGN x = x
+Proof
+  rw[INT_ABS, SGN_def]
+QED
 
 (*--------------------------------------------------------------------------
    INT_MUL_POS_SIGN: thm
    |- !a b. 0 < a ==> 0 < b ==> 0 < a * b
  *--------------------------------------------------------------------------*)
 
-val INT_MUL_POS_SIGN =
-let
-        val lemma01 = #2 (EQ_IMP_RULE (CONJUNCT1 (SPEC_ALL INT_MUL_SIGN_CASES)));
-in
-        store_thm("INT_MUL_POS_SIGN", ``!a:int b:int. 0i<a ==> 0i<b ==> 0i<a * b``, RW_TAC int_ss[lemma01])
-end;
+Theorem INT_MUL_POS_SIGN: !a:int b:int. 0 < a ==> 0 < b ==> 0i < a * b
+Proof
+  rw[INT_MUL_SIGN_CASES]
+QED
 
 (*--------------------------------------------------------------------------
    INT_NE_IMP_LTGT: thm
    |- !x. ~(x = 0) = (0 < x) \/ (x < 0)
  *--------------------------------------------------------------------------*)
 
-Theorem INT_NE_IMP_LTGT: !x. x <> 0i <=> 0i<x \/ x<0i
+Theorem INT_NE_IMP_LTGT: !x:int. x <> 0 <=> 0 < x \/ x < 0
 Proof
-        GEN_TAC THEN
-        EQ_TAC THENL
-        [
-                REWRITE_TAC[IMP_DISJ_THM] THEN
-                PROVE_TAC[INT_LT_TOTAL]
-        ,
-                PROVE_TAC[INT_LT_IMP_NE]
-        ]
+  metis_tac[INT_LT_TOTAL, INT_LT_REFL]
 QED
 
 (*--------------------------------------------------------------------------
@@ -77,35 +88,9 @@ QED
    |- !n. ~(n < 0) = (0 = n) \/ 0 < n
  *--------------------------------------------------------------------------*)
 
-Theorem INT_NOTGT_IMP_EQLT: !n. ~(n < 0i) <=> (0i = n) \/ 0i < n
+Theorem INT_NOTGT_IMP_EQLT: !n:int. ~(n < 0) <=> (0 = n) \/ 0 < n
 Proof
-        GEN_TAC THEN
-        EQ_TAC THEN
-        STRIP_TAC THENL
-        [
-                LEFT_DISJ_TAC THEN
-                PROVE_TAC[INT_LT_TOTAL]
-        ,
-                PROVE_TAC[INT_LT_IMP_NE]
-        ,
-                PROVE_TAC[INT_LT_GT]
-        ]
-QED
-
-(*--------------------------------------------------------------------------
-   INT_NO_ZERODIV : thm
-   |- !x y. (x = 0) \/ (y = 0) = (x * y = 0)
- *--------------------------------------------------------------------------*)
-
-Theorem INT_NO_ZERODIV: !x y. (x = 0i) \/ (y = 0i) = (x * y = 0i)
-Proof
-        REPEAT GEN_TAC THEN
-        ASM_CASES_TAC ``x=0i`` THEN
-        ASM_CASES_TAC ``y=0i`` THEN
-        RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
-        REWRITE_TAC[INT_NE_IMP_LTGT] THEN
-        REWRITE_TAC[INT_MUL_SIGN_CASES] THEN
-        PROVE_TAC[INT_LT_TOTAL]
+  metis_tac[INT_LT_TOTAL, INT_LT_REFL, INT_LT_TRANS]
 QED
 
 (*--------------------------------------------------------------------------
@@ -124,82 +109,50 @@ val INT_NOTPOS0_NEG = store_thm("INT_NOTPOS0_NEG", ``!a. ~(0i<a) ==> ~(a=0i) ==>
    |- !a b. ~(a = 0) ==> ~(b = 0) ==> ~(a * b = 0)
  *--------------------------------------------------------------------------*)
 
-val INT_NOT0_MUL = store_thm("INT_NOT0_MUL", ``!a b. ~(a=0i) ==> ~(b=0i) ==> ~(a*b=0i)``,
-        PROVE_TAC[INT_NO_ZERODIV] );
+Theorem INT_NOT0_MUL: !a b. ~(a=0i) ==> ~(b=0i) ==> ~(a*b=0i)
+Proof
+  PROVE_TAC[INT_ENTIRE]
+QED
 
 (*--------------------------------------------------------------------------
    INT_GT0_IMP_NOT0 : thm
    |- !a. 0 < a ==> ~(a = 0)
  *--------------------------------------------------------------------------*)
 
-val INT_GT0_IMP_NOT0 = store_thm("INT_GT0_IMP_NOT0",``!a. 0i<a ==> ~(a=0i)``,
+Theorem INT_GT0_IMP_NOT0: !a. 0i<a ==> ~(a=0i)
+Proof
         REPEAT STRIP_TAC THEN
         ASM_CASES_TAC ``a = 0i`` THEN
         ASM_CASES_TAC ``a < 0i`` THEN
-        PROVE_TAC[INT_LT_ANTISYM,INT_LT_TOTAL] );
+        PROVE_TAC[INT_LT_ANTISYM,INT_LT_TOTAL]
+QED
 
 (*--------------------------------------------------------------------------
    INT_NOTLTEQ_GT : thm
    |- !a. ~(a < 0) ==> ~(a = 0) ==> 0 < a
  *--------------------------------------------------------------------------*)
 
-val INT_NOTLTEQ_GT = store_thm("INT_NOTLTEQ_GT", ``!a. ~(a<0i) ==> ~(a=0i) ==> 0i<a``,
-        REPEAT STRIP_TAC THEN
-        PROVE_TAC[INT_LT_TOTAL] );
+Theorem INT_NOTLTEQ_GT: !a:int. ~(a<0i) ==> a <> 0 ==> 0 < a
+Proof
+        PROVE_TAC[INT_LT_TOTAL]
+QED
 
 (*--------------------------------------------------------------------------
    INT_ABS_NOT0POS : thm
    |- !x. ~(x = 0) ==> 0 < ABS x
  *--------------------------------------------------------------------------*)
 
-val INT_ABS_NOT0POS = store_thm("INT_ABS_NOT0POS", ``!x:int. ~(x = 0i) ==> 0i < ABS x``,
-        REPEAT STRIP_TAC THEN
-        REWRITE_TAC[INT_ABS] THEN
-        ASM_CASES_TAC ``x<0i`` THENL
-        [
-                RW_TAC int_ss[] THEN
-                ONCE_REWRITE_TAC[GSYM INT_NEG_0] THEN
-                REWRITE_TAC[INT_LT_NEG] THEN
-                PROVE_TAC[]
-        ,
-                RW_TAC int_ss[] THEN
-                UNDISCH_TAC ``~(x < 0i)`` THEN
-                UNDISCH_TAC ``~(x = 0i)`` THEN
-                REWRITE_TAC[IMP_DISJ_THM] THEN
-                PROVE_TAC[INT_LT_TOTAL]
-        ]);
+Theorem INT_ABS_NOT0POS = iffRL INT_ABS_0LT |> GEN_ALL
 
 (*--------------------------------------------------------------------------
    INT_SGN_NOTPOSNEG : thm
    |- !x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)
  *--------------------------------------------------------------------------*)
 
-val INT_SGN_NOTPOSNEG = store_thm("INT_SGN_NOTPOSNEG", ``!x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)``,
-        GEN_TAC THEN
-        REWRITE_TAC[SGN_def] THEN
-        RW_TAC int_ss[] );
-
-(*--------------------------------------------------------------------------
-   INT_SGN_CASES : thm
-   |- !x P.
-        ((SGN x = ~1) /\ (x < 0) ==> P) /\
-        ((SGN x = 0i) /\ (x = 0) ==> P) /\
-        ((SGN x = 1i) /\ (0 < x) ==> P) ==> P
- *--------------------------------------------------------------------------*)
-
-val INT_SGN_CASES = store_thm
-  ("INT_SGN_CASES", ``!x P. ((SGN x = ~1) /\ (x < 0) ==> P) /\
-                            ((SGN x = 0i) /\ (x = 0) ==> P) /\
-                            ((SGN x = 1i) /\ (0 < x) ==> P) ==> P``,
-        REPEAT GEN_TAC THEN
-        ASM_CASES_TAC ``(SGN x = ~1) /\ (x < 0)`` THEN
-        UNDISCH_HD_TAC THEN
-        ASM_CASES_TAC ``(SGN x = 1i) /\ (0 < x)`` THEN
-        UNDISCH_HD_TAC THEN
-        REWRITE_TAC[SGN_def] THEN
-        REWRITE_TAC[DE_MORGAN_THM] THEN
-        RW_TAC int_ss[] THEN
-        PROVE_TAC[INT_LT_TOTAL, INT_SGN_NOTPOSNEG] );
+Theorem INT_SGN_NOTPOSNEG: !x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)
+Proof
+  rw[SGN_def]
+QED
 
 (*--------------------------------------------------------------------------
    LESS_IMP_NOT_0 : thm
@@ -262,100 +215,55 @@ val INT_ABS_CALCULATE_NEG = store_thm("INT_ABS_CALCULATE_NEG", ``!a. a<0 ==> (AB
 val INT_ABS_CALCULATE_0 = store_thm("INT_ABS_CALCULATE_0", ``ABS 0i = 0i``,
         RW_TAC int_ss[INT_ABS] );
 
-(*--------------------------------------------------------------------------
-   INT_ABS_CALCULATE_POS : thm
-   |- !a. 0<a ==> (ABS(a) = a)
- *--------------------------------------------------------------------------*)
-
-val INT_ABS_CALCULATE_POS = store_thm("INT_ABS_CALCULATE_POS", ``!a. 0<a ==> (ABS(a) = a)``,
-        GEN_TAC THEN
-        STRIP_TAC THEN
-        RW_TAC int_ss[INT_ABS, INT_LT_GT] );
+Theorem INT_ABS_CALCULATE_POS: !a. 0<a ==> (ABS(a) = a)
+Proof
+  RW_TAC int_ss[INT_ABS, INT_LT_GT]
+QED
 
 (*--------------------------------------------------------------------------
    INT_NOT0_SGNNOT0 : thm
    |- !x. ~(x = 0) ==> ~(SGN x = 0)
  *--------------------------------------------------------------------------*)
 
-val INT_NOT0_SGNNOT0 = store_thm("INT_NOT0_SGNNOT0", ``!x. ~(x = 0) ==> ~(SGN x = 0)``,
-        REPEAT GEN_TAC THEN
-        STRIP_TAC THEN
-        MATCH_MP_TAC (SPEC ``x:int`` INT_SGN_CASES) THEN
-        REPEAT CONJ_TAC THEN
-        STRIP_TAC  THEN
-        RW_TAC intLib.int_ss [] );
-
-(*--------------------------------------------------------------------------
-   INT_SGN_CLAUSES : thm
-   |- !x. (SGN x = ~1) =
-          (x < 0)) /\ ((SGN x = 0i) = (x = 0)) /\ ((SGN x = 1i) = (x > 0)
- *--------------------------------------------------------------------------*)
-
-val INT_SGN_CLAUSES = store_thm("INT_SGN_CLAUSES", ``!x. ((SGN x = ~1) = (x < 0)) /\ ((SGN x = 0i) = (x = 0)) /\ ((SGN x = 1i) = (x > 0))``,
-        GEN_TAC THEN
-        RW_TAC int_ss[SGN_def] THEN
-        REWRITE_TAC[int_gt] THEN
-        PROVE_TAC[INT_LT_GT, INT_LT_TOTAL] );
-
-(*--------------------------------------------------------------------------
-   INT_SGN_MUL : thm
-   |- !x1 x2 y1 y2. (SGN x1 = y1) ==> (SGN x2 = y2) ==>
-                    (SGN (x1 * x2) = y1 * y2)
- *--------------------------------------------------------------------------*)
-
-val INT_SGN_MUL = store_thm("INT_SGN_MUL", ``!x1 x2 y1 y2. (SGN x1 = y1) ==> (SGN x2 = y2) ==> (SGN (x1 * x2) = y1 * y2)``,
-        REPEAT GEN_TAC THEN
-        REWRITE_TAC[SGN_def] THEN
-        RW_TAC int_ss[] THEN
-        UNDISCH_ALL_TAC THEN
-        RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
-        PROVE_TAC[INT_NO_ZERODIV, INT_MUL_SIGN_CASES, INT_LT_ANTISYM, INT_LT_TOTAL] );
-
-(*--------------------------------------------------------------------------
-   INT_SGN_MUL2 : thm
-   |- !x y. SGN (x * y) = SGN x * SGN y
- *--------------------------------------------------------------------------*)
-
-val INT_SGN_MUL2 = store_thm("INT_SGN_MUL2", ``!x y. SGN (x * y) = SGN x * SGN y``,
-        REPEAT GEN_TAC THEN
-        REWRITE_TAC[SGN_def] THEN
-        RW_TAC int_ss[] THEN
-        UNDISCH_ALL_TAC THEN
-        RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
-        PROVE_TAC[INT_NO_ZERODIV, INT_MUL_SIGN_CASES, INT_LT_ANTISYM, INT_LT_TOTAL] );
-
-(*--------------------------------------------------------------------------
-   INT_SGN_TOTAL : thm
-   |- !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)
- *--------------------------------------------------------------------------*)
-
-val INT_SGN_TOTAL = store_thm("INT_SGN_TOTAL",``!a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)``,
-        GEN_TAC THEN
-        REWRITE_TAC[SGN_def] THEN
-        RW_TAC int_ss[] );
+Theorem INT_NOT0_SGNNOT0:
+  !x. ~(x = 0) ==> ~(SGN x = 0)
+Proof
+  REPEAT GEN_TAC THEN STRIP_TAC THEN
+  MATCH_MP_TAC (SPEC ``x:int`` INT_SGN_CASES) THEN
+  REPEAT CONJ_TAC THEN
+  STRIP_TAC  THEN
+  RW_TAC intLib.int_ss []
+QED
 
-(*--------------------------------------------------------------------------
-   INT_SGN_CASES : thm
-   |- !a P. ((SGN a = ~1) ==> P) /\ ((SGN a = 0i) ==> P) /\
-                                    ((SGN a = 1i) ==> P) ==> P
- *--------------------------------------------------------------------------*)
+Theorem INT_SGN_CLAUSES:
+  !x. (SGN x = ~1 <=> x < 0) /\ (SGN x = 0i <=> x = 0) /\
+      (SGN x = 1i <=> 0 < x)
+Proof
+  GEN_TAC >> qspec_then ‘x’ strip_assume_tac INT_SGN_CASES >>
+  rpt conj_tac >> pop_assum irule >> simp[] >>
+  metis_tac[INT_LT_TRANS, INT_LT_REFL]
+QED
 
-val INT_SGN_CASES = store_thm("INT_SGN_CASES", ``!a P. ((SGN a = ~1) ==> P) /\ ((SGN a = 0i) ==> P) /\ ((SGN a = 1i) ==> P) ==> P``,
-        REPEAT GEN_TAC THEN
-        ASM_CASES_TAC ``SGN a = ~1`` THEN
-        ASM_CASES_TAC ``SGN a = 0i`` THEN
-        ASM_CASES_TAC ``SGN a = 1i`` THEN
-        UNDISCH_ALL_TAC THEN
-        PROVE_TAC[INT_SGN_TOTAL] );
+Theorem INT_SGN_MUL2: !x y. SGN (x * y) = SGN x * SGN y
+Proof
+  REPEAT GEN_TAC THEN
+  REWRITE_TAC[SGN_def] THEN
+  RW_TAC int_ss[] THEN
+  UNDISCH_ALL_TAC THEN
+  RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
+  PROVE_TAC[INT_ENTIRE, INT_MUL_SIGN_CASES, INT_LT_ANTISYM, INT_LT_TOTAL]
+QED
 
 (*--------------------------------------------------------------------------
    INT_LT_ADD_NEG : thm
    |- !x y. x < 0i /\ y < 0i ==> x + y < 0i
  *--------------------------------------------------------------------------*)
 
-val INT_LT_ADD_NEG = store_thm("INT_LT_ADD_NEG", ``!x y. x < 0i /\ y < 0i ==> x + y < 0i``,
+Theorem INT_LT_ADD_NEG: !x y. x < 0i /\ y < 0i ==> x + y < 0i
+Proof
         REWRITE_TAC[GSYM INT_NEG_GT0, INT_NEG_ADD] THEN
-        PROVE_TAC[INT_LT_ADD] );
+        PROVE_TAC[INT_LT_ADD]
+QED
 
 
 val _ = export_theory();
diff --git a/src/rational/ratScript.sml b/src/rational/ratScript.sml
index b491554872..bab4a28011 100644
--- a/src/rational/ratScript.sml
+++ b/src/rational/ratScript.sml
@@ -325,10 +325,13 @@ val RAT_NMRLT0_CONG = store_thm("RAT_NMRLT0_CONG",
   GEN_TAC THEN MATCH_ACCEPT_TAC
     (MATCH_MP RAT_EQUIV_NMR_LTZ_IFF (SPEC_ALL REP_ABS_EQUIV'))) ;
 
-val RAT_NMRGT0_CONG = store_thm("RAT_NMRGT0_CONG",
-  ``!f1. (frac_nmr (rep_rat (abs_rat f1)) > 0) = (frac_nmr f1 > 0)``,
+Theorem RAT_NMRGT0_CONG:
+  !f1. 0 < frac_nmr (rep_rat (abs_rat f1)) <=> 0 < frac_nmr f1
+Proof
   GEN_TAC THEN MATCH_ACCEPT_TAC
-    (MATCH_MP RAT_EQUIV_NMR_GTZ_IFF (SPEC_ALL REP_ABS_EQUIV'))) ;
+    (MATCH_MP (SRULE [int_gt] RAT_EQUIV_NMR_GTZ_IFF)
+              (SPEC_ALL REP_ABS_EQUIV'))
+QED
 
 (*--------------------------------------------------------------------------
  *  RAT_SGN_CONG: thm
@@ -1325,13 +1328,9 @@ val RAT_SGN_MUL = store_thm("RAT_SGN_MUL[simp]",
   REPEAT GEN_TAC THEN REWRITE_TAC[rat_sgn_def, rat_mul_def] THEN
   REWRITE_TAC[RAT_SGN_CONG] THEN PROVE_TAC[FRAC_SGN_MUL2] );
 
-(*--------------------------------------------------------------------------
-   RAT_SGN_MINV: thm
-   |- !r1. ~(r1 = 0q) ==> (rat_sgn (rat_minv r1) = rat_sgn r1)
- *--------------------------------------------------------------------------*)
-
-val RAT_SGN_MINV = store_thm("RAT_SGN_MINV[simp]",
-  ``!r1. ~(r1 = 0q) ==> (rat_sgn (rat_minv r1) = rat_sgn r1)``,
+Theorem RAT_SGN_MINV[simp]:
+  !r1:rat. r1 <> 0 ==> (rat_sgn (rat_minv r1) = rat_sgn r1)
+Proof
   GEN_TAC THEN STRIP_TAC THEN
   REWRITE_TAC[rat_sgn_def, rat_minv_def] THEN
   MATCH_MP_TAC (SPEC ``rep_rat r1`` FRAC_SGN_CASES) THEN
@@ -1343,7 +1342,8 @@ val RAT_SGN_MINV = store_thm("RAT_SGN_MINV[simp]",
   FRAC_NMRDNM_TAC THEN
   RW_TAC int_ss
     [INT_MUL_SIGN_CASES, SGN_def, FRAC_DNMPOS, INT_MUL_LID, int_gt] THEN
-  PROVE_TAC[INT_LT_ANTISYM, int_gt] );
+  PROVE_TAC[INT_LT_ANTISYM, int_gt]
+QED
 
 (*--------------------------------------------------------------------------
    RAT_SGN_TOTAL
@@ -1552,25 +1552,29 @@ val RAT_LEQ_LES_TRANS = store_thm("RAT_LEQ_LES_TRANS",
    |- !r1 r2. r1 < 0q ==> r2 < 0q ==> r1 + r2 < 0q
  *--------------------------------------------------------------------------*)
 
-val RAT_0LES_0LES_ADD = store_thm("RAT_0LES_0LES_ADD",
-  ``!r1 r2. rat_les 0q r1 ==> rat_les 0q r2 ==> rat_les 0q (rat_add r1 r2)``,
+Theorem RAT_0LES_0LES_ADD:
+  !r1 r2. rat_les 0q r1 ==> rat_les 0q r2 ==> rat_les 0q (rat_add r1 r2)
+Proof
   REPEAT GEN_TAC THEN REWRITE_TAC[RAT_0LES_NMR] THEN
   RAT_CALC_TAC THEN FRAC_CALC_TAC THEN
-  REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRGT0_CONG, (GSYM int_gt)] THEN
-  FRAC_NMRDNM_TAC THEN REWRITE_TAC[int_gt] THEN
+  REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRGT0_CONG] THEN
+  FRAC_NMRDNM_TAC THEN
   FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
   FRAC_POS_TAC ``frac_dnm (rep_rat r2)`` THEN
-  REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD] );
+  REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD]
+QED
 
-val RAT_LES0_LES0_ADD = store_thm("RAT_LES0_LES0_ADD",
-  ``!r1 r2. rat_les r1 0q ==> rat_les r2 0q  ==> rat_les (rat_add r1 r2) 0q``,
+Theorem RAT_LES0_LES0_ADD:
+  !r1 r2. rat_les r1 0q ==> rat_les r2 0q  ==> rat_les (rat_add r1 r2) 0q
+Proof
   REPEAT GEN_TAC THEN REWRITE_TAC[RAT_LES0_NMR] THEN
   RAT_CALC_TAC THEN FRAC_CALC_TAC THEN
   REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRLT0_CONG] THEN
-  FRAC_NMRDNM_TAC THEN REWRITE_TAC[int_gt] THEN
+  FRAC_NMRDNM_TAC THEN
   FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
   FRAC_POS_TAC ``frac_dnm (rep_rat r2)`` THEN
-  REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD_NEG] );
+  REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD_NEG]
+QED
 
 (*--------------------------------------------------------------------------
    RAT_0LES_0LEQ_ADD, RAT_LES0_LEQ0_ADD
@@ -2065,7 +2069,7 @@ val RAT_NO_ZERODIV = store_thm("RAT_NO_ZERODIV", ``!r1 r2. (r1 = 0q) \/ (r2 = 0q
         FRAC_CALCTERM_TAC ``frac_mul (rep_rat r1) (rep_rat r2)`` THEN
         REWRITE_TAC[RAT_NMREQ0_CONG] THEN
         FRAC_NMRDNM_TAC THEN
-        PROVE_TAC[INT_NO_ZERODIV] );
+        PROVE_TAC[INT_ENTIRE] );
 
 val RAT_NO_ZERODIV_THM = save_thm(
   "RAT_NO_ZERODIV_THM[simp]",
@@ -2102,59 +2106,6 @@ val LDIV_MUL_OUT = Q.store_thm(
   ‘(r1 / r2) * r3 = (r1 * r3) / r2’,
   metis_tac[RAT_MUL_ASSOC, RAT_DIV_MULMINV, RAT_MUL_COMM]);
 
-(*--------------------------------------------------------------------------
-   RAT_DENSE_THM
-
-   |- !r1 r3. r1 < r3 ==> ?r2. r1 < r2 /\ r2 < r3
- *--------------------------------------------------------------------------*)
-
-val RAT_DENSE_THM =
-let
-        val lemmaZ = prove(``! a b. 0i<b ==> ((a*b > 0i) = (a > 0i))``,
-                REPEAT GEN_TAC THEN
-                STRIP_TAC THEN
-                EQ_TAC THEN
-                SUBST_TAC[SPEC ``b:int`` (GSYM INT_MUL_LZERO)] THEN
-                REWRITE_TAC[UNDISCH_ALL (SPEC ``b:int`` (SPEC ``0i`` (SPEC ``a:int`` (GSYM INT_GT_RMUL_EXP))))] THEN
-                REWRITE_TAC[INT_MUL_LZERO] );
-        val subst1 =
-                EQT_ELIM (INT_RING_CONV ``(frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) + frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1)) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * (2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3)) = frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) * frac_dnm (rep_rat r1)``);
-        val subst2 =
-                EQT_ELIM (INT_RING_CONV ``frac_nmr (rep_rat r3) * (2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3)) + ~(frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) + frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1)) * frac_dnm (rep_rat r3) = frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) * frac_dnm (rep_rat r3)``);
-in
-        store_thm("RAT_DENSE_THM", ``!r1 r3. rat_les r1 r3 ==> ?r2. rat_les r1 r2 /\ rat_les r2 r3``,
-                REPEAT GEN_TAC THEN
-                STRIP_TAC THEN
-                EXISTS_TAC ``abs_rat(abs_frac(rat_nmr r1 * rat_dnm r3 + rat_nmr r3 * rat_dnm r1, 2 * rat_dnm r1 * rat_dnm r3))`` THEN
-                UNDISCH_TAC ``rat_les r1 r3`` THEN
-                REWRITE_TAC[rat_les_def,rat_sgn_def, rat_sub_def] THEN
-                REWRITE_TAC[rat_nmr_def, rat_dnm_def] THEN
-                REWRITE_TAC[RAT_SUB_CONG] THEN
-                REWRITE_TAC[FRAC_SGN_POS] THEN
-                REWRITE_TAC[GSYM int_gt] THEN
-                REWRITE_TAC[RAT_NMRGT0_CONG] THEN
-                REWRITE_TAC[frac_sub_def,frac_ainv_def,frac_add_def] THEN
-                FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
-                FRAC_POS_TAC ``frac_dnm (rep_rat r3)`` THEN
-                FRAC_POS_TAC ``frac_dnm (rep_rat r3) * frac_dnm (rep_rat r1)`` THEN
-                FRAC_POS_TAC ``2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3)`` THEN
-                FRAC_POS_TAC ``2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3) * frac_dnm (rep_rat r1)`` THEN
-                FRAC_POS_TAC ``frac_dnm (rep_rat r3) * (2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3))`` THEN
-                RW_TAC int_ss[NMR,DNM] THENL
-                [
-                        SUBST_TAC[subst1] THEN
-                        REWRITE_TAC[GSYM INT_RDISTRIB] THEN
-                        REWRITE_TAC[UNDISCH_ALL (SPEC ``frac_dnm (rep_rat r1)`` (SPEC ``(frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3))`` lemmaZ))] THEN
-                        PROVE_TAC[]
-                ,
-                        SUBST_TAC[subst2] THEN
-                        REWRITE_TAC[GSYM INT_RDISTRIB] THEN
-                        REWRITE_TAC[UNDISCH_ALL (SPEC ``frac_dnm (rep_rat r3)`` (SPEC ``(frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3))`` lemmaZ))] THEN
-                        PROVE_TAC[]
-                ] )
-end;
-
-
 (*==========================================================================
  * calculation via frac_save terms
  *==========================================================================*)
@@ -2404,6 +2355,13 @@ val RAT_ADD_NUM4 = prove(``!n m. ~&n + ~&m = ~&(n+m)``,
 
 val RAT_ADD_NUM_CALCULATE = save_thm("RAT_ADD_NUM_CALCULATE", LIST_CONJ[RAT_ADD_NUM1, RAT_ADD_NUM2, RAT_ADD_NUM3, RAT_ADD_NUM4] );
 
+Theorem RAT_TIMES2:
+  2 * (x:rat) = x + x
+Proof
+  ‘2n = 1 + 1’ by simp[] >> pop_assum SUBST_ALL_TAC >>
+  REWRITE_TAC[GSYM RAT_ADD_NUM_CALCULATE, RAT_RDISTRIB, RAT_MUL_LID]
+QED
+
 (*--------------------------------------------------------------------------
    RAT_ADD_MUL: thm
 
@@ -2971,6 +2929,17 @@ val RAT_MINV_RATND = Q.store_thm(
 val rat_min_def = Define‘rat_min (r1:rat) r2 = if r1 < r2 then r1 else r2’;
 val rat_max_def = Define‘rat_max (r1:rat) r2 = if r1 > r2 then r1 else r2’;
 
+
+Theorem RAT_DENSE_THM:
+  !r1 r3. r1 < r3 ==> ?r2. r1 < r2 /\ r2 < r3
+Proof
+  rpt strip_tac >>
+  qexists ‘(r1 + r3) / 2’ >>
+  simp[RAT_RDIV_LES_POS, RAT_LDIV_LES_POS, RAT_TIMES2] >>
+  ONCE_REWRITE_TAC[RAT_MUL_COMM] >>
+  simp[RAT_TIMES2, RAT_LES_LADD, RAT_LES_RADD]
+QED
+
 (*==========================================================================
  * end of theory
  *==========================================================================*)