equal
deleted
inserted
replaced
|
1 |
1 (*<*) |
2 (*<*) |
2 theory Paper |
3 theory Paper |
3 imports "../Nominal/Nominal2" |
4 imports "../Nominal/Nominal2" |
4 "~~/src/HOL/Library/LaTeXsugar" |
5 "~~/src/HOL/Library/LaTeXsugar" |
5 begin |
6 begin |
813 %Below we will show the first equation. The others |
814 %Below we will show the first equation. The others |
814 %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
815 %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
815 %we have |
816 %we have |
816 %% |
817 %% |
817 %\begin{equation}\label{abseqiff} |
818 %\begin{equation}\label{abseqiff} |
818 %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; |
819 %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\text{if and only if}\;\; |
819 %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} |
820 %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} |
820 %\end{equation} |
821 %\end{equation} |
821 % |
822 % |
822 %\noindent |
823 %\noindent |
823 %and also |
824 %and also |
824 % |
825 % |