equal
deleted
inserted
replaced
60 by (induct x rule: tr_induct) simp_all |
60 by (induct x rule: tr_induct) simp_all |
61 |
61 |
62 |
62 |
63 subsection {* Case analysis *} |
63 subsection {* Case analysis *} |
64 |
64 |
65 defaultsort pcpo |
65 default_sort pcpo |
66 |
66 |
67 definition |
67 definition |
68 trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where |
68 trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where |
69 ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)" |
69 ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)" |
70 abbreviation |
70 abbreviation |