changeset 5608 | a82a038a3e7a |
parent 5584 | aad639e56d4e |
child 5620 | 3ac11c4af76a |
--- a/src/HOL/UNITY/Common.ML Fri Oct 02 10:44:20 1998 +0200 +++ b/src/HOL/UNITY/Common.ML Fri Oct 02 14:28:39 1998 +0200 @@ -31,7 +31,7 @@ (*** Some programs that implement the safety property above ***) (*This one is just Skip*) -Goal "constrains {id} {m} (maxfg m)"; +Goal "constrains {Id} {m} (maxfg m)"; by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, fasc, gasc]) 1); result();