# HG changeset patch
# User berghofe
# Date 1108144260 -3600
# Node ID 6f43714517ee41167f9aa485c7bf21009975d756
# Parent  b86d5c84a9a7bd521435197da29268c50fb2f2b7
Fully qualified refl and trans to avoid confusion with theorems
in Lattice_Locales.partial_order.

diff -r b86d5c84a9a7 -r 6f43714517ee src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Feb 11 17:11:24 2005 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Feb 11 18:51:00 2005 +0100
@@ -41,12 +41,12 @@
 
    "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
  \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
- \  (trans % TYPE('T) % x % y % z %%  \
+ \  (HOL.trans % TYPE('T) % x % y % z %%  \
  \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
  \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
 
    "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
- \  (refl % TYPE('T) % x)",
+ \  (HOL.refl % TYPE('T) % x)",
 
    "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
  \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
@@ -68,7 +68,7 @@
  \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
  \      (cong % TYPE('T=>bool) % TYPE('T) %  \
  \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
- \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
+ \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
  \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
  \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
@@ -82,7 +82,7 @@
  \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
  \      (cong % TYPE('T=>bool) % TYPE('T) %  \
  \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
- \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
+ \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
  \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
  \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
@@ -92,14 +92,14 @@
    (* All *)
 
    "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
- \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
  \  (allI % TYPE('a) % Q %%  \
  \    (Lam x.  \
  \        iffD1 % P x % Q x %% (prf % x) %%  \
  \         (spec % TYPE('a) % P % x %% prf')))",
 
    "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
- \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
  \  (allI % TYPE('a) % P %%  \
  \    (Lam x.  \
  \        iffD2 % P x % Q x %% (prf % x) %%  \
@@ -108,14 +108,14 @@
    (* Ex *)
 
    "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
- \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
  \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
  \    (Lam x H : P x.  \
  \        exI % TYPE('a) % Q % x %%  \
  \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
 
    "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
- \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
+ \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
  \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
  \    (Lam x H : Q x.  \
  \        exI % TYPE('a) % P % x %%  \
@@ -125,81 +125,81 @@
 
    "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
  \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
- \      (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
+ \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
  \  (conjI % B % D %%  \
  \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
  \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
 
    "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
  \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
- \      (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
+ \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
  \  (conjI % A % C %%  \
  \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
  \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
 
    "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
- \    (refl % TYPE(bool=>bool) % op & A)) ==  \
+ \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
  \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
  \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
- \        (refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
- \        (refl % TYPE(bool) % A)))",
+ \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
+ \        (HOL.refl % TYPE(bool) % A)))",
 
    (* | *)
 
    "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
  \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
- \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
+ \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
  \  (disjE % A % C % B | D %% prf3 %%  \
  \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
  \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
 
    "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
  \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
- \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
+ \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
  \  (disjE % B % D % A | C %% prf3 %%  \
  \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
  \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
 
    "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
- \    (refl % TYPE(bool=>bool) % op | A)) ==  \
+ \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
  \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
  \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
- \        (refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
- \        (refl % TYPE(bool) % A)))",
+ \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
+ \        (HOL.refl % TYPE(bool) % A)))",
 
    (* --> *)
 
    "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
  \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
- \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
+ \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
  \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
  \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
 
    "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
  \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
- \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
+ \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
  \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
  \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
 
    "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
- \    (refl % TYPE(bool=>bool) % op --> A)) ==  \
+ \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
  \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
  \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
- \        (refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
- \        (refl % TYPE(bool) % A)))",
+ \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
+ \        (HOL.refl % TYPE(bool) % A)))",
 
    (* ~ *)
 
    "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
- \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
+ \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
  \  (notI % Q %% (Lam H: Q.  \
  \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
 
    "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
- \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
+ \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
  \  (notI % P %% (Lam H: P.  \
  \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
 
@@ -208,50 +208,50 @@
    "(iffD1 % B % D %%  \
  \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
  \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
- \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
+ \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
  \  (iffD1 % C % D %% prf2 %%  \
  \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
 
    "(iffD2 % B % D %%  \
  \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
  \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
- \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
+ \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
  \  (iffD1 % A % B %% prf1 %%  \
  \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
 
    "(iffD1 % A % C %%  \
  \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
  \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
- \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
+ \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
  \  (iffD2 % C % D %% prf2 %%  \
  \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
 
    "(iffD2 % A % C %%  \
  \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
  \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
- \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
+ \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
  \  (iffD2 % A % B %% prf1 %%  \
  \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
 
    "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
- \    (refl % TYPE(bool=>bool) % op = A)) ==  \
+ \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
  \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
  \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
- \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
- \        (refl % TYPE(bool) % A)))",
+ \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
+ \        (HOL.refl % TYPE(bool) % A)))",
 
    (** transitivity, reflexivity, and symmetry **)
 
-   "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
+   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
  \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
 
-   "(iffD2 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
+   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
  \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
 
-   "(iffD1 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
+   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
 
-   "(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
+   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
 
    "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",