equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Oscar Slotosch |
3 Author: Oscar Slotosch |
4 Copyright 1997 Technische Universitaet Muenchen |
4 Copyright 1997 Technische Universitaet Muenchen |
5 |
5 |
6 *) |
6 *) |
7 open FRACT; |
|
8 |
7 |
9 Goalw [per_def,per_NP_def] |
8 Goalw [per_def,per_NP_def] |
10 "(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; |
9 "(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; |
11 fr refl; |
10 br refl 1; |
12 qed "inst_NP_per"; |
11 qed "inst_NP_per"; |
13 |
12 |
14 |
13 |
15 Goalw [half_def] "half = <[abs_NP(n,2*n)]>"; |
14 Goalw [half_def] "half = <[abs_NP(n,2*n)]>"; |
16 fr per_class_eqI; |
15 br per_class_eqI 1; |
17 by (simp_tac (simpset() addsimps [inst_NP_per]) 1); |
16 by (simp_tac (simpset() addsimps [inst_NP_per]) 1); |
18 qed "test"; |
17 qed "test"; |