2007-10-20 wenzelm 2007-10-20 moved internalM to PrintMode.internal; PrintMode.input;
2007-10-20 wenzelm 2007-10-20 tuned abbrev interface; PrintMode.internal;
2007-10-20 wenzelm 2007-10-20 tuned abbrev interface;
2007-10-20 wenzelm 2007-10-20 added fixed_abbrev;
2007-10-20 wenzelm 2007-10-20 added input/internal, which are never active in print_mode_value;
2007-10-20 wenzelm 2007-10-20 no_variables: tuned error msg;
2007-10-20 wenzelm 2007-10-20 PrintMode.internal;
2007-10-20 wenzelm 2007-10-20 tuned;
2007-10-20 wenzelm 2007-10-20 add_inductive: more careful handling of abbrevs -- do not expand prematurely;
2007-10-20 wenzelm 2007-10-20 fixed proof: neq0_conv;
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-10-20 chaieb 2007-10-20 neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
2007-10-19 wenzelm 2007-10-19 export_code: proper command;
2007-10-19 wenzelm 2007-10-19 warn_open: context position;
2007-10-19 wenzelm 2007-10-19 sorry: proper command;
2007-10-19 wenzelm 2007-10-19 tuned proofs: avoid implicit prems;
2007-10-19 wenzelm 2007-10-19 tuned proofs;
2007-10-19 wenzelm 2007-10-19 internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
2007-10-19 wenzelm 2007-10-19 tuned interfaces;
2007-10-19 haftmann 2007-10-19 tuned
2007-10-19 haftmann 2007-10-19 antisymmetry not a default intro rule any longer
2007-10-19 haftmann 2007-10-19 now employing dictionaries
2007-10-19 haftmann 2007-10-19 added examples
2007-10-19 haftmann 2007-10-19 lemmas with normalization
2007-10-19 wenzelm 2007-10-19 tuned CRITICAL markups;
2007-10-19 wenzelm 2007-10-19 do not export standard_infer_types;
2007-10-19 haftmann 2007-10-19 clarified abbreviations in class context
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute; improved printing of types in interpretations.
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute.
2007-10-19 krauss 2007-10-19 updated
2007-10-19 krauss 2007-10-19 removed funny formatting
2007-10-19 krauss 2007-10-19 Updated function tutorial: Types can be inferred and need not be given anymore
2007-10-19 haftmann 2007-10-19 98% localized
2007-10-19 haftmann 2007-10-19 dropped doubled proof
2007-10-18 krauss 2007-10-18 Simultaneous type inference using read_specification
2007-10-18 paulson 2007-10-18 some more metis calls
2007-10-18 paulson 2007-10-18 Improving the propagation of type constraints for Frees
2007-10-18 paulson 2007-10-18 Ensured that the right number of ATP calls is generated
2007-10-18 haftmann 2007-10-18 CRITICAL evaluation
2007-10-18 haftmann 2007-10-18 improved class syntax
2007-10-18 haftmann 2007-10-18 tuned
2007-10-18 wenzelm 2007-10-18 DeclareRobustCommand \isactrlbsub/esub etc.;
2007-10-18 haftmann 2007-10-18 evaluation is CRITICAL
2007-10-18 haftmann 2007-10-18 moved fork_mixfix to theory_target
2007-10-18 haftmann 2007-10-18 moved lemmas to OrderedGroup.thy
2007-10-18 haftmann 2007-10-18 continued localization
2007-10-18 haftmann 2007-10-18 localized mono predicate
2007-10-17 wenzelm 2007-10-17 removed obsolete unlocalize_mfix;
2007-10-17 wenzelm 2007-10-17 removed obsolete unlocalize_mixfix;
2007-10-17 wenzelm 2007-10-17 locale pred: authentic syntax, tuned aprop_tr' accordingly;
2007-10-17 wenzelm 2007-10-17 store external accesses within name space (as produced by naming policy); improved sticky_prefix: suppress redundant accesses to achieve shorter output; removed unused interfaces; replaced accesses' by external_names (depening on naming);
2007-10-17 wenzelm 2007-10-17 removed unused set_policy;
2007-10-17 wenzelm 2007-10-17 replaced NameSpace.accesses' by NameSpace.external_names (depening on naming);
2007-10-17 nipkow 2007-10-17 added sorted_list_of_set
2007-10-17 wenzelm 2007-10-17 tuned fork_mixfix (back from class.ML);
2007-10-17 wenzelm 2007-10-17 clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
2007-10-17 wenzelm 2007-10-17 removed obsolete fork_mixfix (back to theory_target.ML);
2007-10-17 wenzelm 2007-10-17 updated;
2007-10-16 haftmann 2007-10-16 clarified fork_mixfix
2007-10-16 haftmann 2007-10-16 exported standard_term_check