%------------------------------------------------------------------------- % % Theory of bags and finite bags. Version 2.0 7/29/96 % % Authors: Rick Butler NASA Langley Research Center % David Griffioen CWI (National Research Institute for % Mathematics and Computer Science % and KUN (Catholic University Nijmegen), % the Netherlands. % % bags : fundamental definitions and properties % bags_aux : definition of filter, rest, and choose % bags_to_sets : converts bags to sets % finite_bags : basic definitions and lemmas % finite_bags_lems : lemmas need induction % finite_bags_aux : lemmas about filter, rest, and choose % finite_bags_inductions : induction schemes %------------------------------------------------------------------------ top: THEORY BEGIN IMPORTING bags, bags_aux, bags_to_sets, finite_bags_lems, finite_bags_aux, finite_bags_inductions END top