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" |
4 "../Nominal/Nominal2_Eqvt" |
5 "../Nominal/Atoms" |
5 "../Nominal/Atoms" |
6 "../Nominal/Abs" |
6 "../Nominal/Nominal2_Abs" |
7 "LaTeXsugar" |
7 "LaTeXsugar" |
8 begin |
8 begin |
9 |
9 |
10 notation (latex output) |
10 notation (latex output) |
11 sort_of ("sort _" [1000] 100) and |
11 sort_of ("sort _" [1000] 100) and |
312 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
312 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
313 \begin{tabular}{@ {}l} |
313 \begin{tabular}{@ {}l} |
314 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
314 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
315 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
315 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
316 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm} |
316 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm} |
317 @{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} |
317 @{thm diff_def[where M="\<pi>\<^isub>1" and N="\<pi>\<^isub>2"]} |
318 \end{tabular} |
318 \end{tabular} |
319 \end{isabelle} |
319 \end{isabelle} |
320 |
320 |
321 \noindent |
321 \noindent |
322 and verify the simple properties |
322 and verify the simple properties |