equal
deleted
inserted
replaced
1 (* Title: HOLCF/One.ML |
1 (* Title: HOLCF/One.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Oscar Slotosch |
3 Author: Oscar Slotosch |
4 Copyright 1997 Technische Universitaet Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 The unit domain |
6 The unit domain. |
7 *) |
7 *) |
8 |
8 |
9 (* ------------------------------------------------------------------------ *) |
9 (* ------------------------------------------------------------------------ *) |
10 (* Exhaustion and Elimination for type one *) |
10 (* Exhaustion and Elimination for type one *) |
11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
12 |
12 |
13 Goalw [ONE_def] "t=UU | t = ONE"; |
13 Goalw [ONE_def] "t=UU | t = ONE"; |
14 by (lift.induct_tac "t" 1); |
14 by (induct_tac "t" 1); |
15 by (Simp_tac 1); |
15 by (Simp_tac 1); |
16 by (Simp_tac 1); |
16 by (Simp_tac 1); |
17 qed "Exh_one"; |
17 qed "Exh_one"; |
18 |
18 |
19 val prems = Goal "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"; |
19 val prems = Goal "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"; |