author | paulson |
Fri, 13 Nov 1998 13:41:53 +0100 | |
changeset 5858 | beddc19c107a |
parent 5069 | 3ea049f7979d |
child 6162 | 484adda70b65 |
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 |
||
5069 | 8 |
Goalw [per_def,per_NP_def] |
3842 | 9 |
"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; |
5858 | 10 |
br refl 1; |
2906 | 11 |
qed "inst_NP_per"; |
12 |
||
13 |
||
5069 | 14 |
Goalw [half_def] "half = <[abs_NP(n,2*n)]>"; |
5858 | 15 |
br per_class_eqI 1; |
4089 | 16 |
by (simp_tac (simpset() addsimps [inst_NP_per]) 1); |
2906 | 17 |
qed "test"; |