src/HOL/AxClasses/Tutorial/Xor.ML

Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML

(*  Title:      HOL/AxClasses/Tutorial/Xor.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Proof the instantiation theorem bool :: agroup by hand.
*)

open AxClass;

goal_arity Xor.thy ("bool", [], "agroup");
by (axclass_tac Xor.thy []);
by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
by (ALLGOALS (fast_tac HOL_cs));
qed "bool_in_agroup";