2001-09-27 wenzelm renamed real_of_int_eq_iff to real_of_int_inject;
2001-09-27 wenzelm document setup;
2001-09-27 wenzelm new-style theory;
2001-09-27 wenzelm Square roots of primes are irrational;
2001-09-27 wenzelm AddXIs [dvdI]; AddXEs [dvdE];
2001-09-27 wenzelm tuned;
2001-09-27 wenzelm tuned;
2001-09-27 wenzelm tuned;
2001-09-27 wenzelm AddXEs [UnI1, UnI2];
2001-09-27 wenzelm AddXEs [disjI1, disjI2];
2001-09-27 wenzelm ex/Hilbert_Classical.thy ex/document/root.tex;
2001-09-27 wenzelm tuned;
2001-09-27 wenzelm document setup;
2001-09-27 wenzelm derive tertium-non-datur by means of Hilbert's choice operator;
2001-09-27 wenzelm obsolete;
2001-09-27 wenzelm updated;
2001-09-27 wenzelm -v option;
2001-09-27 wenzelm verbose option;
2001-09-27 wenzelm use_dir: verbose option;
2001-09-27 wenzelm removed option -d (now standard behaviour);
2001-09-27 wenzelm option -v;
2001-09-26 wenzelm activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
2001-09-26 wenzelm updated;
2001-09-26 wenzelm tuned order;
2001-09-26 wenzelm bold symbols;
2001-09-26 wenzelm tuned;
2001-09-26 wenzelm turn bullet into bold cdot (looks much better in printed output);
2001-09-26 wenzelm use darkblue for all links;
2001-09-26 wenzelm updated;
2001-09-25 wenzelm updated;
2001-09-25 wenzelm *** empty log message ***
2001-09-25 wenzelm tuned;
2001-09-21 oheimb Minor improvements, added Example
2001-09-17 wenzelm tuned;
2001-09-13 berghofe Fixed proof term bug in permute_prems.
2001-09-12 wenzelm result_error_default: include msg;
2001-09-11 nipkow *** empty log message ***
2001-09-10 oheimb marginally improved comments
2001-09-10 oheimb corrected antiquotations in comment
2001-09-10 oheimb simplified vnam/vname, introduced fname, improved comments
2001-09-10 wenzelm tuned usage;
2001-09-08 wenzelm print_state: subgoals;
2001-09-08 wenzelm export pretty_goals;
2001-09-08 wenzelm result_error_default: output *single* error message;
2001-09-08 wenzelm tuned;
2001-09-08 wenzelm ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);
2001-09-08 wenzelm * system: support Poly/ML 4.1.1 (large heaps);
2001-09-08 wenzelm smart selection of isabelle-process versus isabelle-interface;
2001-09-04 wenzelm renamed "antecedent" case to "rule_context";
2001-09-04 nipkow *** empty log message ***
2001-09-03 nipkow *** empty log message ***
2001-08-31 wenzelm tuned;
2001-08-31 wenzelm final proofs := 0;
2001-08-31 wenzelm HOL-Real-Hyperreal made a plain session (no longer an image);
2001-08-31 wenzelm renamed `keep_derivs' to `proofs', and made an integer;
2001-08-31 wenzelm * Proof General keywords specification is now part of the Isabelle
2001-08-31 wenzelm proper use of invent_names;
2001-08-31 wenzelm fixed header;
2001-08-31 wenzelm tuned headers;
2001-08-31 wenzelm keyword classification tables for Isabelle/Isar Proof General
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip