isabelle: Graph

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

A stronger apply_0, and new thm domain_lam
1998-07-17, by paulson
added comments
1998-07-17, by paulson
tidying
1998-07-17, by paulson
now with Goal cmd
1998-07-17, by paulson
tidying
1998-07-16, by paulson
Got rid of obsolete "goal" commands.
1998-07-16, by paulson
Addition of "Theorem B" of Peter Andrews
1998-07-16, by paulson
Fixed bug in transform_rule.
1998-07-15, by berghofe
More tidying and removal of "\!\!... from Goal commands
1998-07-15, by paulson
More tidying and removal of "\!\!... from Goal commands
1998-07-15, by paulson
@ -> $
1998-07-15, by nipkow
disjoint
1998-07-15, by nipkow
Minor tidying up.
1998-07-15, by nipkow
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
added unit_eq simplification procedure;
1998-06-25, by wenzelm
added XX_YY_rewrite: simpset -> cterm -> thm;
1998-06-25, by wenzelm
Thm.rewrite_cterm;
1998-06-25, by wenzelm
defaults for free variables hide consts of same name;
1998-06-25, by wenzelm
added rewrite_cterm;
1998-06-25, by wenzelm
Installation of target HOL-Real
1998-06-25, by paulson
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
1998-06-24, by nipkow
Ran isatool fixgoal
1998-06-24, by paulson
removed duplicate entry for Goal
1998-06-24, by paulson
Trivial change to be more like paper
1998-06-24, by paulson
Tidying; renaming of Says_Server_message_form to
1998-06-24, by paulson
*** empty log message ***
1998-06-23, by nipkow
Consequences of the change from [ := ] to ( := ) in theory Update.
1998-06-23, by nipkow
Replaced [ := ] syntax by ( := ).
1998-06-23, by nipkow
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
1998-06-22, by paulson
comments and minor tidying
1998-06-22, by paulson
simplified and tidied the proofs
1998-06-22, by paulson
check_mlhome_file;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
def_sort;
1998-06-20, by wenzelm
renamed Thm(s) back to thm(s);
1998-06-20, by wenzelm
export mk_triple1/2;
1998-06-20, by wenzelm
added read_def_axm;
1998-06-20, by wenzelm
added fix_mixfix;
1998-06-20, by wenzelm
fixed comment
1998-06-19, by paulson
tidying
1998-06-19, by paulson
New example Kerberos_BAN by G Bella
1998-06-19, by paulson
fixed comment;
1998-06-18, by wenzelm
tuned \s pattern;
1998-06-18, by wenzelm
isatool fixgoal;
1998-06-18, by wenzelm
removed Thy;
1998-06-18, by wenzelm
replaced warning by error_msg;
1998-06-18, by wenzelm
new toplevel commands `Goal' and `Goalw';
1998-06-18, by wenzelm
renamed thm(s) to Thm(s);
1998-06-18, by wenzelm
replace goal(w) commands by implicit versions Goal(w);
1998-06-18, by wenzelm
Goal and Goalw
1998-06-17, by nipkow
goal -> Goal
1998-06-17, by nipkow
Changed and changed back.
1998-06-17, by nipkow
Goals may now contain assumptions, which are not returned.
1998-06-17, by nipkow
added General/history.ML;
1998-06-16, by wenzelm
Histories of values, with undo and redo;
1998-06-16, by wenzelm
use_text replaces use_strings;
1998-06-15, by wenzelm
handle_error: capture error msgs, even if no exception raised;
1998-06-15, by wenzelm