MultisetOrder mmoved to HOL/Library;
authorwenzelm
Wed Oct 18 23:35:56 2000 +0200 (2000-10-18)
changeset 1025721055ac27708
parent 10256 320a4084dfac
child 10258 d549f2534e6d
MultisetOrder mmoved to HOL/Library;
src/HOL/Isar_examples/ROOT.ML
src/HOL/Isar_examples/document/root.tex
     1.1 --- a/src/HOL/Isar_examples/ROOT.ML	Wed Oct 18 23:35:08 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Wed Oct 18 23:35:56 2000 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  time_use_thy "Summation";
     1.5  time_use_thy "KnasterTarski";
     1.6  time_use_thy "MutilatedCheckerboard";
     1.7 -with_path "../Induct"       time_use_thy "MultisetOrder";
     1.8  with_path "../W0"           time_use_thy "W_correct";
     1.9  with_path "../NumberTheory" time_use_thy "Fibonacci";
    1.10  time_use_thy "Puzzle";
     2.1 --- a/src/HOL/Isar_examples/document/root.tex	Wed Oct 18 23:35:08 2000 +0200
     2.2 +++ b/src/HOL/Isar_examples/document/root.tex	Wed Oct 18 23:35:56 2000 +0200
     2.3 @@ -31,10 +31,6 @@
     2.4  \input{Summation.tex}
     2.5  \input{KnasterTarski.tex}
     2.6  \input{MutilatedCheckerboard.tex}
     2.7 -%\input{Multiset0.tex}
     2.8 -%\input{Acc.tex}
     2.9 -%\input{Multiset.tex}
    2.10 -\input{MultisetOrder.tex}
    2.11  %\input{Maybe.tex}
    2.12  %\input{Type.tex}
    2.13  \input{W_correct.tex}