src/HOL/Recdef.thy
changeset 16417 9bc16273c2d4
parent 15481 fc075ae929e4
child 17040 6682c93b7d9f
     1.1 --- a/src/HOL/Recdef.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory Recdef
     1.6  imports Wellfounded_Relations Datatype
     1.7 -files
     1.8 +uses
     1.9    ("../TFL/casesplit.ML")
    1.10    ("../TFL/utils.ML")
    1.11    ("../TFL/usyntax.ML")