2007-11-13 berghofe 2007-11-13 Removed some case_names and consumes attributes that are now no longer needed due to changes in the to_pred and to_set attributes.
2007-11-13 berghofe 2007-11-13 Added TrueE to extraction_expand.
2007-11-13 berghofe 2007-11-13 Added new program extraction examples.
2007-11-13 berghofe 2007-11-13 New case studies for program extraction.
2007-11-13 berghofe 2007-11-13 Moved auxiliary lemmas to separate theory.
2007-11-13 berghofe 2007-11-13 Added new exampes Greatest_Common_Divisor and Euclid.
2007-11-13 berghofe 2007-11-13 Moved nat_eq_dec to Util.thy
2007-11-13 berghofe 2007-11-13 Moved nat_eq_dec and search to Util.thy
2007-11-13 berghofe 2007-11-13 Tuned.
2007-11-13 berghofe 2007-11-13 to_pred and to_set now save induction and case rule tags.
2007-11-12 wenzelm 2007-11-12 removed left-over text links from lynx conversion; removed umlauts (cannot assume iso-latin anymore, and not yet utf-8 either);
2007-11-12 wenzelm 2007-11-12 back to sigusr2, after Poly/ML 5.1 has been adapted;
2007-11-12 wenzelm 2007-11-12 changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
2007-11-12 nipkow 2007-11-12 updates
2007-11-12 haftmann 2007-11-12 updated
2007-11-12 wenzelm 2007-11-12 reactivated default paragraph formatting for ``proof documents'';
2007-11-12 schirmer 2007-11-12 fixed typo;
2007-11-12 schirmer 2007-11-12 added signatures; tuned
2007-11-11 wenzelm 2007-11-11 abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; export standard_infer_types;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; dest;
2007-11-11 nipkow 2007-11-11 updates
2007-11-11 wenzelm 2007-11-11 avoid ML print in production code;
2007-11-11 wenzelm 2007-11-11 updated;
2007-11-11 wenzelm 2007-11-11 auto quickcheck: reduced messages;
2007-11-11 wenzelm 2007-11-11 notation works with any known constant (including fixes/abbrevs);
2007-11-11 wenzelm 2007-11-11 HOL-Statespace;
2007-11-11 wenzelm 2007-11-11 * HOL-Statespace;
2007-11-11 wenzelm 2007-11-11 restore interrupt handler on init;
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;