2007-11-11 wenzelm 2007-11-11 abbrev: back to PrintMode.internal, which works at least half-way;
2007-11-11 wenzelm 2007-11-11 syntax operations: turned extend'' into update'' (absorb duplicates); tuned signature;
2007-11-11 wenzelm 2007-11-11 replaced extend_prtabs by update_prtabs (absorb duplicates);
2007-11-11 wenzelm 2007-11-11 abbrev: PrintMode.input instead of PrintMode.internal for global version!
2007-11-11 wenzelm 2007-11-11 renamed update_list to cons_list; added proper update_list (based on Library.update);
2007-11-11 wenzelm 2007-11-11 syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11 wenzelm 2007-11-11 renamed Symtab.update_list to Symtab.cons_list;
2007-11-11 wenzelm 2007-11-11 tuned specifications of 'notation';
2007-11-10 wenzelm 2007-11-10 added update_const_gram (avoids duplicates); tuned;
2007-11-10 wenzelm 2007-11-10 remove_prtabs: tuned, avoid excessive garbage;
2007-11-10 wenzelm 2007-11-10 update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10 wenzelm 2007-11-10 similar_types: uniform treatment of TFrees/TVars;
2007-11-10 wenzelm 2007-11-10 notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10 wenzelm 2007-11-10 tuned specifications of 'notation';
2007-11-10 wenzelm 2007-11-10 removed LocalTheory.target_naming/name;
2007-11-10 wenzelm 2007-11-10 put_inductives: be permissive about multiple versions (target names are not necessarily unique); add_inductive: store info under global (!) name -- very rough approximation of the real thing;
2007-11-10 wenzelm 2007-11-10 tuned proofs; tuned document;
2007-11-10 wenzelm 2007-11-10 tuned document;
2007-11-10 wenzelm 2007-11-10 Orderings.min/max: no need to qualify consts; removed legacy ML bindings;
2007-11-10 wenzelm 2007-11-10 auto_quickcheck ref: set default in ProofGeneral/preferences only (retains responsiveness of plain tty interaction); auto_quickcheck: more messages, less complicated code;
2007-11-10 wenzelm 2007-11-10 ProofGeneral/preferences: auto_quickcheck=true;
2007-11-10 wenzelm 2007-11-10 qualified Proofterm.proofs;
2007-11-10 wenzelm 2007-11-10 @{const}: improved ProofContext.read_const does the job;
2007-11-10 wenzelm 2007-11-10 locale_const: suppress in class body as well (prevents qualified printing);
2007-11-10 wenzelm 2007-11-10 notation: improved ProofContext.read_const does the job;
2007-11-10 wenzelm 2007-11-10 updated;
2007-11-10 wenzelm 2007-11-10 replaced @{const} (allows name only) by proper @{term};
2007-11-09 haftmann 2007-11-09 proper implementation of check phase; non-qualified names for class operations
2007-11-09 haftmann 2007-11-09 explicit message for failed autoquickcheck
2007-11-09 wenzelm 2007-11-09 tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-09 wenzelm 2007-11-09 avoid obsolete Sign.read_prop;
2007-11-09 wenzelm 2007-11-09 tuned proofs -- avoid implicit prems;
2007-11-09 wenzelm 2007-11-09 fixed imports path;
2007-11-09 wenzelm 2007-11-09 tuned proofs -- avoid open cases;
2007-11-09 krauss 2007-11-09 function package: using the names of the equations as case names turned out to be impractical => disabled
2007-11-09 krauss 2007-11-09 avoid name clashes when generating code for union, inter
2007-11-08 wenzelm 2007-11-08 oops -- avoid vacous goal message; tuned messages;
2007-11-08 wenzelm 2007-11-08 tuned messages; tuned;
2007-11-08 wenzelm 2007-11-08 avoid "import" as identifier, which is a keyword in Alice;
2007-11-08 wenzelm 2007-11-08 tuned presentation;
2007-11-08 wenzelm 2007-11-08 avoid implicit use of prems; tuned proofs;
2007-11-08 wenzelm 2007-11-08 where/of: do not allow schematic variables here!
2007-11-08 wenzelm 2007-11-08 removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy; discontinued legacy_intern_skolem, gen_read';
2007-11-08 wenzelm 2007-11-08 discontinued legacy vars;
2007-11-08 wenzelm 2007-11-08 removed unused read_def_terms';
2007-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of;
2007-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of; tuned;
2007-11-08 wenzelm 2007-11-08 x86_64: fall back on x86 (more efficient);
2007-11-08 wenzelm 2007-11-08 tuned comments;
2007-11-08 wenzelm 2007-11-08 renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-08 wenzelm 2007-11-08 renamed ProofContext.read_const' to ProofContext.read_const_proper; export expand_abbrevs;
2007-11-08 wenzelm 2007-11-08 synchronize_syntax: improved declare_const (still inactive); tuned;
2007-11-08 wenzelm 2007-11-08 added const_proper;
2007-11-08 nipkow 2007-11-08 added evaluation
2007-11-08 nipkow 2007-11-08 fix
2007-11-08 nipkow 2007-11-08 new general syntax
2007-11-08 nipkow 2007-11-08 tuned
2007-11-08 nipkow 2007-11-08 updated to notation and abbreviation
2007-11-08 haftmann 2007-11-08 added purify_sym
2007-11-08 haftmann 2007-11-08 tuned