author | wenzelm |
Fri, 01 Sep 1995 14:27:36 +0200 | |
changeset 1247 | 18b1441fb603 |
child 1899 | 0075a8d26a80 |
permissions | -rw-r--r-- |
1247 | 1 |
(* Title: HOL/AxClasses/Tutorial/Xor.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Proof the instantiation theorem bool :: agroup by hand. |
|
6 |
*) |
|
7 |
||
8 |
open AxClass; |
|
9 |
||
10 |
goal_arity Xor.thy ("bool", [], "agroup"); |
|
11 |
by (axclass_tac Xor.thy []); |
|
12 |
by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]); |
|
13 |
by (ALLGOALS (fast_tac HOL_cs)); |
|
14 |
qed "bool_in_agroup"; |