equal
deleted
inserted
replaced
80 (* inequality *) |
80 (* inequality *) |
81 val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>"; |
81 val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>"; |
82 by (cut_facts_tac prems 1); |
82 by (cut_facts_tac prems 1); |
83 by (rtac notI 1); |
83 by (rtac notI 1); |
84 by (dtac per_class_eqE 1); |
84 by (dtac per_class_eqE 1); |
85 by (Auto_tac()); |
85 by Auto_tac; |
86 qed "per_class_neqI"; |
86 qed "per_class_neqI"; |
87 |
87 |
88 val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>"; |
88 val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>"; |
89 by (cut_facts_tac prems 1); |
89 by (cut_facts_tac prems 1); |
90 by (rtac notI 1); |
90 by (rtac notI 1); |
91 by (dtac er_class_eqE 1); |
91 by (dtac er_class_eqE 1); |
92 by (Auto_tac()); |
92 by Auto_tac; |
93 qed "er_class_neqI"; |
93 qed "er_class_neqI"; |
94 |
94 |
95 val prems = goal thy "<[x]>~=<[y]>==>~x===y"; |
95 val prems = goal thy "<[x]>~=<[y]>==>~x===y"; |
96 by (cut_facts_tac prems 1); |
96 by (cut_facts_tac prems 1); |
97 by (rtac notI 1); |
97 by (rtac notI 1); |