equal
deleted
inserted
replaced
6 |
6 |
7 theory Sprod |
7 theory Sprod |
8 imports Bifinite |
8 imports Bifinite |
9 begin |
9 begin |
10 |
10 |
11 defaultsort pcpo |
11 default_sort pcpo |
12 |
12 |
13 subsection {* Definition of strict product type *} |
13 subsection {* Definition of strict product type *} |
14 |
14 |
15 pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) = |
15 pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) = |
16 "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" |
16 "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" |