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

tuned;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
lookup long names of types;
1997-10-20, by wenzelm
tuned qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
qualified names;
1997-10-20, by wenzelm
local;
1997-10-20, by wenzelm
Sign.base_name;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
tuned output;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
Sign.base_name;
1997-10-20, by wenzelm
fixed types of add_XXX;
1997-10-20, by wenzelm
local;
1997-10-20, by wenzelm
local section;
1997-10-20, by wenzelm
addsplits
1997-10-18, by nipkow
adapted to qualified names;
1997-10-17, by wenzelm
no longer tries bogus eta-contract involving aprops;
1997-10-17, by wenzelm
adapted to qualified names;
1997-10-17, by wenzelm
fixed RAW target;
1997-10-17, by wenzelm
(co) inductive / datatype package adapted to qualified names;
1997-10-17, by wenzelm
obselete 'end' hack;
1997-10-17, by wenzelm
global;
1997-10-17, by wenzelm
tuned "." syntax;
1997-10-17, by wenzelm
removed Classlib;
1997-10-17, by wenzelm
*** empty log message ***
1997-10-17, by wenzelm
setloop split_tac -> addsplits
1997-10-17, by nipkow
Added error messages.
1997-10-17, by nipkow
A lot of new comments
1997-10-17, by paulson
Eta-expanded a function decl to make sml/nj happy
1997-10-17, by paulson
Added "op" before "occs" to make sml/nj happy
1997-10-17, by paulson
New rewrite rules for simplifying conditionals
1997-10-17, by paulson
New trivial rewrites
1997-10-17, by paulson
New rewrite rules for simplifying conditionals
1997-10-17, by paulson
Better simplification eliminates a command from proof of psubset_card
1997-10-17, by paulson
New simprules imp_disj1,2 and some comments
1997-10-17, by paulson
Added image_eqI to simpset.
1997-10-17, by nipkow
Removed image_eqI from simpset because of clash with neq_shrK.
1997-10-17, by nipkow
AddIffs [all_not_in_conv];
1997-10-16, by nipkow
global;
1997-10-16, by wenzelm
Modified comment.
1997-10-16, by nipkow
New simprules imp_disj1, imp_disj2
1997-10-16, by paulson
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
1997-10-16, by paulson
Removed comment.
1997-10-16, by nipkow
tuned;
1997-10-16, by wenzelm
removed begin;
1997-10-16, by wenzelm
fixed prep_ext;
1997-10-16, by wenzelm
Simplified proof.
1997-10-16, by nipkow
Simplified proof because of better simplifier.
1997-10-16, by nipkow
Various new lemmas. Improved conversion of equations to rewrite rules:
1997-10-16, by nipkow
added transfer: theory -> thm -> thm;
1997-10-16, by wenzelm
oops;
1997-10-16, by wenzelm
The simplifier has been improved a little: equations s=t which used to be
1997-10-16, by nipkow
fixed dependencies;
1997-10-16, by wenzelm
transfer thy Ord_nat;
1997-10-16, by wenzelm
sevaral goals restated in mono.thy;
1997-10-16, by wenzelm
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
1997-10-16, by wenzelm
transfer InfDatatype.thy Limit_VfromE;
1997-10-16, by wenzelm
transfer CardinalArith.thy nat_into_Ord;
1997-10-16, by wenzelm

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

isabelle