equal
deleted
inserted
replaced
97 |
97 |
98 (*** Injectiveness ***) |
98 (*** Injectiveness ***) |
99 |
99 |
100 (** Atomic nodes **) |
100 (** Atomic nodes **) |
101 |
101 |
102 goalw Univ.thy [Atom_def] "inj(Atom)"; |
102 goalw Univ.thy [Atom_def, inj_def] "inj(Atom)"; |
103 by (rtac injI 1); |
103 by (fast_tac (prod_cs addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1); |
104 by (etac (singleton_inject RS Abs_Node_inject RS Pair_inject) 1); |
|
105 by (REPEAT (ares_tac [Node_K0_I] 1)); |
|
106 qed "inj_Atom"; |
104 qed "inj_Atom"; |
107 val Atom_inject = inj_Atom RS injD; |
105 val Atom_inject = inj_Atom RS injD; |
108 |
106 |
109 goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)"; |
107 goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)"; |
110 by (rtac injI 1); |
108 by (rtac injI 1); |