equal
deleted
inserted
replaced
|
1 (* Title: HOL/IOA/example/Lemmas.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 (Mostly) Arithmetic lemmas |
|
7 Should realy go in Arith.ML. |
|
8 Also: Get rid of all the --> in favour of ==> !!! |
|
9 *) |
|
10 |
1 (* Logic *) |
11 (* Logic *) |
2 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; |
12 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; |
3 by(fast_tac (HOL_cs addDs prems) 1); |
13 by(fast_tac (HOL_cs addDs prems) 1); |
4 val imp_conj_lemma = result(); |
14 val imp_conj_lemma = result(); |
5 |
15 |