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