equal
deleted
inserted
replaced
5 |
5 |
6 *) |
6 *) |
7 open NPAIR; |
7 open NPAIR; |
8 |
8 |
9 goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np"; |
9 goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np"; |
10 auto(); |
10 by (Auto_tac()); |
11 qed "rep_abs_NP"; |
11 qed "rep_abs_NP"; |
12 |
12 |
13 Addsimps [rep_abs_NP]; |
13 Addsimps [rep_abs_NP]; |
14 |
14 |
15 val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x"; |
15 val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x"; |
16 by (cut_facts_tac prems 1); |
16 by (cut_facts_tac prems 1); |
17 auto(); |
17 by (Auto_tac()); |
18 qed "per_sym_NP"; |
18 qed "per_sym_NP"; |
19 |
19 |