equal
deleted
inserted
replaced
852 first equation of Theorem \ref{suppabs}. The others follow by similar |
852 first equation of Theorem \ref{suppabs}. The others follow by similar |
853 arguments. By definition of the abstraction type @{text |
853 arguments. By definition of the abstraction type @{text |
854 "abs\<^bsub>set\<^esub>"} we have |
854 "abs\<^bsub>set\<^esub>"} we have |
855 |
855 |
856 \begin{equation}\label{abseqiff} |
856 \begin{equation}\label{abseqiff} |
857 @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; |
857 @{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; |
858 @{term "alpha_set_ex (as, x) equal supp (bs, y)"} |
858 @{term "alpha_set_ex (as, x) equal supp (bs, y)"} |
859 \end{equation}\smallskip |
859 \end{equation}\smallskip |
860 |
860 |
861 \noindent |
861 \noindent |
862 and also |
862 and also |