# HG changeset patch
# User haftmann
# Date 1173426358 -3600
# Node ID 1c38ca2496c4fc3783850e1278f934771d687653
# Parent  c252770ae2d0e38acc2b61e720bcc9d2687535cd
resolved name clashes

diff -r c252770ae2d0 -r 1c38ca2496c4 src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Fri Mar 09 08:45:57 2007 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Fri Mar 09 08:45:58 2007 +0100
@@ -340,21 +340,21 @@
 by (unfold uniq_def, blast)
 
 constdefs ord :: "proto => (rule => rule => bool) => bool"
-"ord p inf == ALL R R'. R:p --> R':p --> ~ inf R R' --> inf R' R"
+"ord p inff == ALL R R'. R:p --> R':p --> ~ inff R R' --> inff R' R"
 
-lemma ordD: "[| ord p inf; ~ inf R R'; R:p; R':p |] ==> inf R' R"
+lemma ordD: "[| ord p inff; ~ inff R R'; R:p; R':p |] ==> inff R' R"
 by (unfold ord_def, blast)
 
 constdefs uniq' :: "proto => (rule => rule => bool) => secfun => bool"
-"uniq' p inf secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
-inf R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
+"uniq' p inff secret == ALL evs R R' n n' Ks s s'. R:p --> R':p -->
+inff R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' -->
 Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} -->
 apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks -->
 evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) -->
 secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) -->
 secret R n s Ks = secret R' n' s' Ks"
 
-lemma uniq'D: "[| uniq' p inf secret; evs: tr p; inf R R'; R:p; R':p; n:newn R;
+lemma uniq'D: "[| uniq' p inff secret; evs: tr p; inff R R'; R:p; R':p; n:newn R;
 n':newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs);
 Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'};
 secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs);
@@ -362,10 +362,10 @@
 secret R n s Ks = secret R' n' s' Ks"
 by (unfold uniq'_def, blast)
 
-lemma uniq'_imp_uniq: "[| uniq' p inf secret; ord p inf |] ==> uniq p secret"
+lemma uniq'_imp_uniq: "[| uniq' p inff secret; ord p inff |] ==> uniq p secret"
 apply (unfold uniq_def)
 apply (rule allI)+
-apply (case_tac "inf R R'")
+apply (case_tac "inff R R'")
 apply (blast dest: uniq'D)
 by (auto dest: ordD uniq'D intro: sym)
 
diff -r c252770ae2d0 -r 1c38ca2496c4 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Fri Mar 09 08:45:57 2007 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Fri Mar 09 08:45:58 2007 +0100
@@ -806,8 +806,8 @@
                 G\<turnstile>(Class class) accessible_in (pid accclass);
                 membr=(C,mdecl new);
                 G\<turnstile>(C,new) overrides\<^sub>S old; 
-                G\<turnstile>class \<prec>\<^sub>C sup;
-                G\<turnstile>Method old of sup accessible_from accclass
+                G\<turnstile>class \<prec>\<^sub>C supr;
+                G\<turnstile>Method old of supr accessible_from accclass
                \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
 
 syntax 
@@ -848,8 +848,8 @@
 | Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
                 membr=(C,mdecl new);
                 G\<turnstile>(C,new) overrides old; 
-                G\<turnstile>class \<prec>\<^sub>C sup;
-                G\<turnstile>Method old in sup dyn_accessible_from accclass
+                G\<turnstile>class \<prec>\<^sub>C supr;
+                G\<turnstile>Method old in supr dyn_accessible_from accclass
                \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
 
 syntax 
diff -r c252770ae2d0 -r 1c38ca2496c4 src/HOL/Lattice/Bounds.thy
--- a/src/HOL/Lattice/Bounds.thy	Fri Mar 09 08:45:57 2007 +0100
+++ b/src/HOL/Lattice/Bounds.thy	Fri Mar 09 08:45:58 2007 +0100
@@ -7,6 +7,9 @@
 
 theory Bounds imports Orders begin
 
+hide const inf sup
+hide const inf sup
+
 subsection {* Infimum and supremum *}
 
 text {*