author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4089 | 96fba19bcbe2 |
child 5858 | beddc19c107a |
permissions | -rw-r--r-- |
2906 | 1 |
(* Title: HOL/Quot/FRACT.ML |
2 |
ID: $Id$ |
|
3 |
Author: Oscar Slotosch |
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
|
5 |
||
6 |
*) |
|
7 |
open FRACT; |
|
8 |
||
5069 | 9 |
Goalw [per_def,per_NP_def] |
3842 | 10 |
"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; |
2906 | 11 |
fr refl; |
12 |
qed "inst_NP_per"; |
|
13 |
||
14 |
||
5069 | 15 |
Goalw [half_def] "half = <[abs_NP(n,2*n)]>"; |
2906 | 16 |
fr per_class_eqI; |
4089 | 17 |
by (simp_tac (simpset() addsimps [inst_NP_per]) 1); |
2906 | 18 |
qed "test"; |