| changeset 16417 | 9bc16273c2d4 |
| parent 14765 | bafb24c150c1 |
| child 18413 | 50c0c118e96d |
--- a/src/HOL/Induct/SList.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Induct/SList.thy Fri Jun 17 16:12:49 2005 +0200 @@ -24,7 +24,7 @@ Tidied by lcp. Still needs removal of nat_rec. *) -theory SList = NatArith + Sexp + Hilbert_Choice: +theory SList imports NatArith Sexp Hilbert_Choice begin (*Hilbert_Choice is needed for the function "inv"*)