| changeset 16417 | 9bc16273c2d4 |
| parent 15647 | b1f486a9c56b |
| child 17566 | 484ff733f29c |
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Jun 17 16:12:49 2005 +0200 @@ -3,7 +3,7 @@ Author: Sebastian Skalberg (TU Muenchen) *) -theory GenHOL4Real = GenHOL4Base: +theory GenHOL4Real imports GenHOL4Base begin import_segment "hol4";