equal
deleted
inserted
replaced
10 |
10 |
11 (*Eliminates a commonly-occurring expression*) |
11 (*Eliminates a commonly-occurring expression*) |
12 goal HOL.thy "~ (ALL x. x~=y)"; |
12 goal HOL.thy "~ (ALL x. x~=y)"; |
13 by (Blast_tac 1); |
13 by (Blast_tac 1); |
14 Addsimps [result()]; |
14 Addsimps [result()]; |
15 |
|
16 open Message; |
|
17 |
15 |
18 AddIffs atomic.inject; |
16 AddIffs atomic.inject; |
19 AddIffs msg.inject; |
17 AddIffs msg.inject; |
20 |
18 |
21 (*Equations hold because constructors are injective; cannot prove for all f*) |
19 (*Equations hold because constructors are injective; cannot prove for all f*) |