changeset 41460 | ea56b98aee83 |
parent 17589 | 58eeffd73be1 |
child 58889 | 5b7a9633cfa8 |
41441:a7a03f856354 | 41460:ea56b98aee83 |
---|---|
1 (* Title: HOL/ex/Intuitionistic.thy |
1 (* Title: HOL/ex/Intuitionistic.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
5 |
4 |
6 Taken from FOL/ex/int.ML |
5 Taken from FOL/ex/int.ML |
7 *) |
6 *) |