src/HOL/AxClasses/Tutorial/Xor.ML
author nipkow
Fri, 04 Apr 1997 16:03:44 +0200
changeset 2907 0e272e4c7cb2
parent 1899 0075a8d26a80
child 6393 b8dafa978382
permissions -rw-r--r--
inv -> inverse

(*  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.inverse_bool_def, Xor.unit_bool_def]);
by (ALLGOALS (Fast_tac));
qed "bool_in_agroup";