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

fixed arity;
1999-08-25, by wenzelm
expand_classes renamed to intro_classes;
1999-08-25, by wenzelm
TPHOLs99;
1999-08-25, by wenzelm
Removed "Adding axioms ..." message.
1999-08-25, by berghofe
hide private parts;
1999-08-25, by wenzelm
another snapshot
1999-08-25, by paulson
arguably clearer definition of the inductive case of
1999-08-25, by paulson
tidied
1999-08-25, by paulson
new guarantees laws; also better natural deduction style for old ones
1999-08-25, by paulson
renamed some theorems; also better natural deduction style for old ones
1999-08-25, by paulson
project constants
1999-08-25, by paulson
many "project" laws
1999-08-25, by paulson
new guarantees laws; also better natural deduction style for old ones
1999-08-25, by paulson
split_paired_Eps and lemmas
1999-08-25, by paulson
new theorem inv_f_eq
1999-08-25, by paulson
%dir;
1999-08-24, by wenzelm
tuned;
1999-08-24, by wenzelm
draft release;
1999-08-24, by wenzelm
Real/Real.thy main entry point;
1999-08-24, by wenzelm
isar: no_pos flag;
1999-08-24, by wenzelm
fixed add_sect etc.;
1999-08-24, by wenzelm
??thesis: include params;
1999-08-24, by wenzelm
print_mode activated again;
1999-08-24, by wenzelm
fixed intro_elim_tac;
1999-08-24, by wenzelm
record_simproc;
1999-08-23, by wenzelm
tuned;
1999-08-23, by wenzelm
record_simproc;
1999-08-23, by wenzelm
Some changes in sections about Sum and Nat.
1999-08-23, by berghofe
simplifier flex heads.
1999-08-23, by nipkow
Now rewrite rules with flexible heads are allowed.
1999-08-23, by nipkow
isatool expandshort;
1999-08-23, by wenzelm
tuned;
1999-08-23, by wenzelm
Moved sum_case to theory HOL/Datatype.
1999-08-23, by berghofe
tuned;
1999-08-23, by wenzelm
Corrected two busg in the simplifier.
1999-08-23, by nipkow
\indexisarreg;
1999-08-22, by wenzelm
\VVar;
1999-08-22, by wenzelm
checkpoint;
1999-08-22, by wenzelm
tuned;
1999-08-22, by wenzelm
real numerals;
1999-08-21, by wenzelm
added HOL-Real;
1999-08-21, by wenzelm
echo ML_PLATFORM;
1999-08-20, by wenzelm
activate example;
1999-08-20, by wenzelm
delcongs [if_weak_cong];
1999-08-20, by wenzelm
print_context;
1999-08-20, by wenzelm
eliminated HOL-AxClasses target;
1999-08-20, by wenzelm
intro (no +);
1999-08-20, by wenzelm
mucke -res;
1999-08-20, by wenzelm
if_svc_enabled;
1999-08-20, by wenzelm
AxClasses, Isar_examples;
1999-08-20, by wenzelm
intro/elim: REPEAT1;
1999-08-20, by wenzelm
new theories RealBin, RealInt, RealPow
1999-08-20, by paulson
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
1999-08-19, by wenzelm
quite a lot of tuning and cleanup;
1999-08-19, by wenzelm
sysman: Stefan Berghofer;
1999-08-19, by wenzelm
more;
1999-08-19, by wenzelm
Mucke, Einhoven;
1999-08-19, by wenzelm
quite a lot of tuning an cleanup;
1999-08-19, by wenzelm
sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.
1999-08-19, by berghofe
Moved sum_case stuff from Sum to Datatype.
1999-08-19, by berghofe

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

isabelle