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

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

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

isabelle