equal
deleted
inserted
replaced
727 show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales |
727 show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales |
728 fix x y |
728 fix x y |
729 show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" |
729 show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" |
730 by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric]) |
730 by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric]) |
731 qed |
731 qed |
732 print_interps logic_o (* FIXME *) |
732 print_interps logic_o |
733 thm loc.lor_o_def por_eq |
|
734 have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def) |
733 have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def) |
735 } |
734 } |
736 qed |
735 qed |
737 |
736 |
738 end |
737 end |