author | wenzelm |
Wed, 17 Mar 1999 16:53:32 +0100 | |
changeset 6393 | b8dafa978382 |
parent 6392 | e2ecfd8622ae |
child 6394 | 3d9fd50fcc43 |
--- a/src/HOL/AxClasses/Tutorial/Xor.ML Wed Mar 17 16:45:53 1999 +0100 +++ b/src/HOL/AxClasses/Tutorial/Xor.ML Wed Mar 17 16:53:32 1999 +0100 @@ -8,7 +8,7 @@ open AxClass; goal_arity Xor.thy ("bool", [], "agroup"); -by (axclass_tac Xor.thy []); +by (axclass_tac []); by (rewrite_goals_tac [Xor.prod_bool_def,Xor.inverse_bool_def, Xor.unit_bool_def]); by (ALLGOALS (Fast_tac));