author | kleing |
Fri, 21 Jun 2013 16:21:33 -0700 | |
changeset 52405 | 3dd63180cdbf |
parent 52404 | 33524382335b |
child 52406 | 1e57c3c4e05c |
--- a/src/HOL/IMP/Types.thy Fri Jun 21 16:20:47 2013 +0200 +++ b/src/HOL/IMP/Types.thy Fri Jun 21 16:21:33 2013 -0700 @@ -2,6 +2,9 @@ theory Types imports Star Complex_Main begin +text {* We build on @{theory Complex_Main} instead of @{theory Main} to access +the real numbers. *} + subsection "Arithmetic Expressions" datatype val = Iv int | Rv real