| changeset 7179 | 6ffe5067d5cc |
| parent 6676 | 62d1e642da30 |
| child 7221 | 13e43b7456a1 |
--- a/src/HOL/UNITY/Handshake.ML Thu Aug 05 22:11:07 1999 +0200 +++ b/src/HOL/UNITY/Handshake.ML Thu Aug 05 22:11:43 1999 +0200 @@ -15,9 +15,6 @@ program_defs_ref := [F_def, G_def]; Addsimps (map simp_of_act [cmdF_def, cmdG_def]); - -(*Simplification for records*) -Addsimps (thms"state.update_defs"); Addsimps [simp_of_set invFG_def];