isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Removal of leading "\!\!..." from most Goal commands
1998-07-15, by paulson
new stac
1998-07-14, by paulson
CHANGED_GOAL added to declare a more robust stac
1998-07-14, by paulson
inj_on
1998-07-14, by nipkow
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
1998-07-14, by paulson
Corrected dead link.
1998-07-13, by nipkow
Huge tidy-up: removal of leading \!\!
1998-07-13, by paulson
massive tidying of proofs
1998-07-13, by paulson
renamed mutex to Acts
1998-07-13, by paulson
Replace awkward primrec by recdef.
1998-07-13, by nipkow
swapped condition in update_apply.
1998-07-13, by nipkow
isatool expandshort;
1998-07-12, by wenzelm
the distribution now includes Isabelle icons: see
1998-07-10, by wenzelm
added xpm icons;
1998-07-10, by wenzelm
Converted to Auto_tac
1998-07-06, by nipkow
several new basic modules made available for general use;
1998-07-03, by wenzelm
cleaned up;
1998-07-03, by wenzelm
theory Main includes everything;
1998-07-03, by wenzelm
reorganized the main HOL image;
1998-07-03, by wenzelm
stepping stones: Recdef, Main;
1998-07-03, by wenzelm
stepping stones;
1998-07-03, by wenzelm
removed duplicate thms;
1998-07-03, by wenzelm
moved String theory to main HOL;
1998-07-03, by wenzelm
Removed disjE from list of rules used to simplify elimination
1998-07-03, by berghofe
Removed leading !! in goals
1998-07-03, by nipkow
Removed leading !! in goals.
1998-07-03, by nipkow
Removed leading !! in goals.
1998-07-03, by nipkow
Renamed expand_if to split_if and setloop split_tac to addsplits,
1998-07-02, by paulson
HACKED declaration of addsplits
1998-07-02, by paulson
Deleted leading parameters thanks to new Goal command
1998-07-02, by paulson
tuned comment;
1998-07-02, by wenzelm
Symbol.beginning;
1998-07-02, by wenzelm
Uncurried functions LeadsTo and reach
1998-07-02, by paulson
fixed Integ;
1998-07-02, by wenzelm
Adapted to new inductive definition package.
1998-07-01, by berghofe
Fixed bug (improper handling of flag no_ind).
1998-07-01, by berghofe
Replaced "use_dir" command by "use", because nested calls
1998-07-01, by berghofe
HOL-Real
1998-07-01, by paulson
tuned Inductive.thy;
1998-07-01, by wenzelm
added add_typedecls;
1998-07-01, by wenzelm
Removed structure Prod_Syntax.
1998-06-30, by berghofe
Adapted to new inductive definition package.
1998-06-30, by berghofe
Adapted to new inductive package.
1998-06-30, by berghofe
Removed obsolete comments.
1998-06-30, by berghofe
Removed old inductive definition package.
1998-06-30, by berghofe
Removed structure Prod_Syntax.
1998-06-30, by berghofe
Adapted to new inductive definition package.
1998-06-30, by berghofe
Moved most of the Prod_Syntax - stuff to HOLogic.
1998-06-30, by berghofe
Added additional theorems needed for inductive definitions.
1998-06-30, by berghofe
New inductive definition package
1998-06-30, by berghofe
added quick_and_dirty flag;
1998-06-30, by wenzelm
moved actual (C)Pure theories to pure.ML;
1998-06-29, by wenzelm
tuned transaction;
1998-06-29, by wenzelm
use_text: verbose flag;
1998-06-29, by wenzelm
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-26, by paulson
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-26, by paulson
fixed unit_eq;
1998-06-25, by wenzelm
delsimprocs [unit_eq_proc];
1998-06-25, by wenzelm
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
1998-06-25, by wenzelm
tuned loose bound vars check;
1998-06-25, by wenzelm

less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle