# HG changeset patch # User nipkow # Date 907924539 -7200 # Node ID ac627075b808a1a6e8068aaea26d985737ac5dcb # Parent f67c34721486dde10e3f897cb2d3ef885a3278f3 added Induct/Multiset* diff -r f67c34721486 -r ac627075b808 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 09 11:15:07 1998 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 09 11:15:39 1998 +0200 @@ -81,6 +81,8 @@ Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \ Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \ Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \ + Induct/Multiset0.ML Induct/Multiset0.thy \ + Induct/Multiset.ML Induct/Multiset.thy \ Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \ Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/Simult.ML \ Induct/Simult.thy Induct/Term.ML Induct/Term.thy