| author | wenzelm |
| Tue, 27 May 1997 15:45:07 +0200 | |
| changeset 3362 | 0b268cff9344 |
| parent 2907 | 0e272e4c7cb2 |
| child 6393 | b8dafa978382 |
| permissions | -rw-r--r-- |
(* 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";