equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Nominal/Nominal2_Base" |
3 imports "../Nominal/Nominal2_Base" |
4 "../Nominal/Nominal2_Eqvt" |
|
5 "../Nominal/Atoms" |
4 "../Nominal/Atoms" |
6 "LaTeXsugar" |
5 "LaTeXsugar" |
7 begin |
6 begin |
8 |
7 |
9 notation (latex output) |
8 notation (latex output) |
344 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
343 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
345 \begin{tabular}{@ {}l} |
344 \begin{tabular}{@ {}l} |
346 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
345 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
347 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
346 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
348 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm} |
347 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm} |
349 @{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} |
348 @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} |
350 \end{tabular} |
349 \end{tabular} |
351 \end{isabelle} |
350 \end{isabelle} |
352 |
351 |
353 \noindent |
352 \noindent |
354 and verify the simple properties |
353 and verify the simple properties |