| changeset 2445 | 51993fea433f |
| parent 2444 | 150644698367 |
| child 2446 | c2a9bf6c0948 |
| 2444:150644698367 | 2445:51993fea433f |
|---|---|
1 (* Title: HOLCF/holcfb.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Changed by: David von Oheimb |
|
5 Copyright 1993 Technische Universitaet Muenchen |
|
6 *) |
|
7 |
|
8 |
|
9 open Holcfb; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* Some lemmas in HOL.thy *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 |
|
16 |
|
17 val classical3 = (notE RS notI); (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *) |