equal
deleted
inserted
replaced
19 (* Use {x. False} = {}? *) |
19 (* Use {x. False} = {}? *) |
20 |
20 |
21 Goalw [atom_def,step_def] |
21 Goalw [atom_def,step_def] |
22 "eps(atom a) = {}"; |
22 "eps(atom a) = {}"; |
23 by (Simp_tac 1); |
23 by (Simp_tac 1); |
24 by (Blast_tac 1); |
|
25 qed "eps_atom"; |
24 qed "eps_atom"; |
26 Addsimps [eps_atom]; |
25 Addsimps [eps_atom]; |
27 |
26 |
28 Goalw [atom_def,step_def] |
27 Goalw [atom_def,step_def] |
29 "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)"; |
28 "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)"; |