renamed twos-compl.ML to twos_compl.ML
authorclasohm
Thu Nov 04 14:12:31 1993 +0100 (1993-11-04)
changeset 9130c8e9c380a2
parent 90 a90653dabebc
child 92 7252e7699e24
renamed twos-compl.ML to twos_compl.ML
src/ZF/ex/ROOT.ML
     1.1 --- a/src/ZF/ex/ROOT.ML	Thu Nov 04 14:11:59 1993 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Thu Nov 04 14:12:31 1993 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  time_use_thy "ex/equiv";
     1.5  time_use_thy "ex/integ";
     1.6  (*Binary integer arithmetic*)
     1.7 -use          "ex/twos-compl.ML";
     1.8 +use          "ex/twos_compl.ML";
     1.9  time_use     "ex/bin.ML";
    1.10  time_use_thy "ex/binfn";
    1.11