author | paulson |
Wed, 15 Jul 1998 10:15:13 +0200 | |
changeset 5143 | b94cd208f073 |
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";