author | nipkow |
Fri, 04 Apr 1997 16:03:44 +0200 | |
changeset 2907 | 0e272e4c7cb2 |
parent 1899 | 0075a8d26a80 |
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";