2004-05-21 ago wenzelm test_classrel/arity improve error reporting; tuned;
2004-05-21 ago wenzelm xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
2004-05-21 ago wenzelm string_of_vname moved to term.ML;
2004-05-21 ago wenzelm incorporate sort ops from term.ML; use Graph.T; misc cleanup;
2004-05-21 ago wenzelm type.ML now before Syntax module;
2004-05-21 ago wenzelm xxx_typ_raw replace xxx_typ_no_norm forms;
2004-05-21 ago wenzelm 'classrel' now allows multiple arguments;
2004-05-21 ago wenzelm Sign.certify_tyname;
2004-05-21 ago wenzelm TypeInfer.paramify_dummies, TypeInfer.param;
2004-05-21 ago wenzelm Args.local_typ_raw;
2004-05-21 ago wenzelm output_tym: removed duplicate clauses;
2004-05-21 ago wenzelm Graph.minimals;
2004-05-21 ago wenzelm adapted syntax to cope with lack of non-logical types;
2004-05-21 ago wenzelm Type.typ_instance;
2004-05-21 ago wenzelm load ML files only once;
2004-05-21 ago wenzelm removed duplicate thms;
2004-05-21 ago wenzelm Sign.typ_instance;
2004-05-21 ago wenzelm tuned message;
2004-05-21 ago wenzelm tuned document;
2004-05-21 ago wenzelm use plain SOME;
2004-05-21 ago wenzelm proper use of 'syntax';
2004-05-19 ago paulson auto update
2004-05-19 ago paulson has_consts now handles the @-operator
2004-05-19 ago paulson new bij_betw operator
2004-05-19 ago paulson more results about isomorphisms
2004-05-19 ago paulson conversion of Hilbert_Choice to Isar script
2004-05-19 ago chaieb the function list1 has been exported.
2004-05-19 ago chaieb A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
2004-05-19 ago chaieb tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
2004-05-18 ago obua modified abel_cancel.ML for polymorphic types
2004-05-18 ago obua simplification for abelian groups
2004-05-18 ago obua Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
2004-05-17 ago webertj Comments fixed
2004-05-17 ago mehta lemma disjoint_int_union removed - too special
2004-05-14 ago ballarin Change of theory hierarchy: Group is now based in Lattice.
2004-05-14 ago paulson tidied
2004-05-14 ago paulson new atomize theorem
2004-05-14 ago paulson removed a premise of card_inj_on_le
2004-05-14 ago paulson removal of locale coset
2004-05-14 ago paulson deleted redundant proof lines
2004-05-14 ago paulson new lemmas
2004-05-14 ago paulson clauses for ordinary resolution
2004-05-14 ago paulson conversion of theorems to atomic form
2004-05-13 ago mehta New simp rules added:
2004-05-12 ago paulson simpilified and strengthened proofs
2004-05-12 ago nipkow fixed latex problems
2004-05-12 ago nipkow renamed `> to o_m
2004-05-11 ago obua changes made due to new Ring_and_Field theory
2004-05-11 ago berghofe Eta-expanded function scan_comment to make SmlNJ happy.
2004-05-11 ago paulson broken no longer includes TTP, and other minor changes
2004-05-11 ago paulson removal of prime characters
2004-05-11 ago paulson package needed for superscripts
2004-05-11 ago paulson conversion to clauses for ordinary resolution rather than ME
2004-05-11 ago paulson auto update
2004-05-10 ago wenzelm Pure: nested comments in inner syntax;
2004-05-10 ago wenzelm support nested comments;
2004-05-10 ago wenzelm changed Symbol.beginning;
2004-05-10 ago wenzelm tuned;
2004-05-10 ago wenzelm Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);
2004-05-10 ago wenzelm added Scan.list;