src/HOL/ex/ROOT.ML
changeset 39639 a1aa9fbcbd3d
parent 39404 b98909faaea8
child 40495 c4336e45f199
     1.1 --- a/src/HOL/ex/ROOT.ML	Wed Sep 15 13:44:10 2010 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Sep 15 13:44:10 2010 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4    "Efficient_Nat_examples",
     1.5    "FuncSet",
     1.6    "Eval_Examples",
     1.7 -  "NormalForm"
     1.8 +  "Normalization_by_Evaluation"
     1.9  ];
    1.10  
    1.11  use_thys [