changeset 6393 | b8dafa978382 |
parent 2907 | 0e272e4c7cb2 |
--- 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));