equal
deleted
inserted
replaced
351 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
351 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
352 \begin{tabular}{@ {}l} |
352 \begin{tabular}{@ {}l} |
353 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
353 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
354 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
354 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
355 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm} |
355 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm} |
356 @{thm diff_def[where x="\<pi>\<^isub>1" and y="\<pi>\<^isub>2"]} |
356 @{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} |
357 \end{tabular} |
357 \end{tabular} |
358 \end{isabelle} |
358 \end{isabelle} |
359 |
359 |
360 \noindent |
360 \noindent |
361 and verify the simple properties |
361 and verify the simple properties |