equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Slides2 |
2 theory Slides2 |
3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal" |
3 imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2" |
4 begin |
4 begin |
5 |
5 |
6 notation (latex output) |
6 notation (latex output) |
7 set ("_") and |
7 set ("_") and |
8 Cons ("_::/_" [66,65] 65) |
8 Cons ("_::/_" [66,65] 65) |
383 \pause |
383 \pause |
384 \isanewline |
384 \isanewline |
385 |
385 |
386 {\small\begin{tabular}{rcl} |
386 {\small\begin{tabular}{rcl} |
387 @{text "sort_ty (TVar x)"} & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\ |
387 @{text "sort_ty (TVar x)"} & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\ |
388 @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}\\ |
388 @{text "sort_ty (\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^sub>1, sort_ty \<tau>\<^sub>2]"}\\ |
389 \end{tabular}} |
389 \end{tabular}} |
390 \pause |
390 \pause |
391 \isanewline\isanewline |
391 \isanewline\isanewline |
392 \isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"} |
392 \isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"} |
393 \pause |
393 \pause |