changeset 9403 | aad13b59b8d9 |
parent 7523 | 3a716ebc2fc0 |
--- a/src/HOL/UNITY/Handshake.ML Fri Jul 21 17:46:43 2000 +0200 +++ b/src/HOL/UNITY/Handshake.ML Fri Jul 21 18:01:36 2000 +0200 @@ -19,7 +19,7 @@ by (rtac AlwaysI 1); by (Force_tac 1); by (rtac (constrains_imp_Constrains RS StableI) 1); -by (auto_tac (claset(), simpset() addsimps [Join_constrains])); +by Auto_tac; by (constrains_tac 2); by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset())); by (constrains_tac 1);