1998-11-09 wenzelm 1998-11-09 added metacuts_tac;
1998-11-09 wenzelm 1998-11-09 removed local_theory;
1998-11-09 wenzelm 1998-11-09 exnMessage Interrupt;
1998-11-09 wenzelm 1998-11-09 added lift_modifier, rule;
1998-11-09 wenzelm 1998-11-09 added Isar;
1998-11-09 wenzelm 1998-11-09 added Isar/;
1998-11-09 wenzelm 1998-11-09 Pure outer syntax.
1998-11-09 wenzelm 1998-11-09 Non-logical toplevel commands.
1998-11-09 wenzelm 1998-11-09 Derived theory operations.
1998-11-09 wenzelm 1998-11-09 The global Isabelle/Isar outer syntax.
1998-11-09 wenzelm 1998-11-09 The Isabelle/Isar toplevel.
1998-11-09 wenzelm 1998-11-09 Histories of proof states, with undo / redo and prev / back.
1998-11-09 wenzelm 1998-11-09 Generic parsers for Isabelle/Isar outer syntax.
1998-11-09 wenzelm 1998-11-09 Outer lexical syntax for Isabelle/Isar.
1998-11-09 wenzelm 1998-11-09 Proof methods.
1998-11-09 wenzelm 1998-11-09 Symbolic theorem attributes.
1998-11-09 wenzelm 1998-11-09 Concrete argument syntax (for attributes, methods etc.).
1998-11-09 wenzelm 1998-11-09 Type-safe interface for proof context data.
1998-11-09 wenzelm 1998-11-09 Proof states and methods.
1998-11-09 wenzelm 1998-11-09 Proof context information.
1998-11-09 wenzelm 1998-11-09 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
1998-11-09 wenzelm 1998-11-09 Check release name and date in NEWS!
1998-11-09 wenzelm 1998-11-09 smart interrupt handler;
1998-11-09 wenzelm 1998-11-09 option -I: startup Isar interaction mode;
1998-11-09 wenzelm 1998-11-09 isabelle -I;
1998-11-09 wenzelm 1998-11-09 fake interrupt handler;
1998-11-09 wenzelm 1998-11-09 simple interrupt_handler;
1998-11-09 paulson 1998-11-09 new Domain/Range rules
1998-11-09 paulson 1998-11-09 new TIMES/Sigma rules
1998-11-09 paulson 1998-11-09 removed obsolete comment and "open" declaration
1998-11-06 paulson 1998-11-06 "Subscribe" link
1998-11-06 wenzelm 1998-11-06 spell check;
1998-11-06 wenzelm 1998-11-06 tuned;
1998-11-06 mueller 1998-11-06 added mailing list, removed mirrors;
1998-11-06 paulson 1998-11-06 Revising the Client proof as suggested by Michel Charpentier. New lemmas about composition (in Union.ML), etc. Also changed "length" to "size" because it is displayed as "size" in any event.
1998-11-05 mueller 1998-11-05 made more generic;
1998-11-05 nipkow 1998-11-05 Shortened names and added new thm.
1998-11-04 paulson 1998-11-04 Some streamlining of text. Theory library is now assumed to be LOCAL and not at TUM.
1998-11-03 wenzelm 1998-11-03 tuned;
1998-11-03 wenzelm 1998-11-03 tuned width of pics;
1998-11-03 wenzelm 1998-11-03 tuned;
1998-11-02 wenzelm 1998-11-02 oops;
1998-11-02 wenzelm 1998-11-02 tuned pics;
1998-11-02 wenzelm 1998-11-02 made weblint happy;
1998-11-02 wenzelm 1998-11-02 oops;
1998-11-02 wenzelm 1998-11-02 Id;
1998-11-02 wenzelm 1998-11-02 tuned; fixed links;
1998-11-02 wenzelm 1998-11-02 tuned;
1998-11-02 wenzelm 1998-11-02 main Isabelle page;
1998-11-02 nipkow 1998-11-02 New example
1998-11-02 paulson 1998-11-02 Domain r, Range r replace fst``r, snd``r
1998-11-02 paulson 1998-11-02 increased precedence of unary minus from 80 to 100 requires a similar increase for %# and %%#
1998-11-02 paulson 1998-11-02 increased precedence of unary minus from 80 to 100
1998-10-31 paulson 1998-10-31 Charpentier laws
1998-10-31 paulson 1998-10-31 the Increasing operator
1998-10-31 paulson 1998-10-31 no need for int_0
1998-10-31 paulson 1998-10-31 locales now implicitly quantify over free variables
1998-10-30 wenzelm 1998-10-30 tuned current_goals_markers;
1998-10-30 paulson 1998-10-30 Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
1998-10-30 paulson 1998-10-30 Explicit (and improved) simprules for binary arithmetic. New default simprules to eliminate (int 0) and (z + - w)