equal
deleted
inserted
replaced
680 |
680 |
681 lemma (in Rsemi_rev) r_assoc: |
681 lemma (in Rsemi_rev) r_assoc: |
682 "(x ++ y) ++ z = x ++ (y ++ z)" |
682 "(x ++ y) ++ z = x ++ (y ++ z)" |
683 by (simp add: r_def assoc) |
683 by (simp add: r_def assoc) |
684 |
684 |
685 lemma (in Rpair_semi) |
|
686 includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65) |
|
687 constrains prod :: "['a, 'a] => 'a" |
|
688 and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair" |
|
689 shows "(x +++ y) +++ z = x +++ (y +++ z)" |
|
690 apply (rule r_assoc) done |
|
691 |
|
692 |
685 |
693 subsection {* Import of Locales with Predicates as Interpretation *} |
686 subsection {* Import of Locales with Predicates as Interpretation *} |
694 |
687 |
695 locale Ra = |
688 locale Ra = |
696 assumes Ra: "True" |
689 assumes Ra: "True" |