isabelle: Graph

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

tuned;
1997-10-24, by wenzelm
Modified comment.
1997-10-24, by nipkow
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
1997-10-24, by nipkow
HOL/Map
1997-10-24, by nipkow
Added the new theory Map.
1997-10-24, by nipkow
added record section;
1997-10-23, by wenzelm
Sign.name_of;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
improved typ parser, exported;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
hide id, stamps;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
added sort_wrt;
1997-10-23, by wenzelm
fixed prune of hidden short names;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
tuned;
1997-10-22, by wenzelm
certify: check_stale;
1997-10-22, by wenzelm
improved handling of draft signatures / theories; draft thms (and
1997-10-21, by wenzelm
sg_ref: automatic adjustment of thms of draft theories;
1997-10-21, by wenzelm
commit;
1997-10-21, by wenzelm
made Poly/ML happy, but SML/NJ unhappy;
1997-10-21, by wenzelm
typo
1997-10-21, by nipkow
Corrected alphabetical order of entries in signature.
1997-10-21, by nipkow
Fixed the index entries for "recursion, general"
1997-10-21, by paulson
Many minor speedups:
1997-10-21, by paulson
New rewrite rules image_iff
1997-10-21, by paulson
Documented `addsplits'
1997-10-20, by nipkow
make SML/NJ happy;
1997-10-20, by wenzelm
rm IOA TLA;
1997-10-20, by wenzelm
tuned types;
1997-10-20, by wenzelm
tuned sig;
1997-10-20, by wenzelm
reset global_names;
1997-10-20, by wenzelm
set global_names;
1997-10-20, by wenzelm
replaced ops by consts;
1997-10-20, by wenzelm
removed Dlist;
1997-10-20, by wenzelm
\label{simp-chap} -> chap:simplification
1997-10-20, by nipkow
fixed goal_XXX;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
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
improved pretty_arity;
1997-10-16, by wenzelm
added merge_theories (new name arg);
1997-10-16, by wenzelm
fixed merge_theories;
1997-10-16, by wenzelm
revert to 1.3;
1997-10-16, by wenzelm
revert to 1.1;
1997-10-16, by wenzelm
Added last, butlast, dropped ttl.
1997-10-16, by nipkow
lala
1997-10-16, by mueller
Eta-expansion of function declarations, for value polymorphism
1997-10-16, by paulson
remove merge_theories;
1997-10-15, by wenzelm
make_draft replaced by prep_ext;
1997-10-15, by wenzelm
tuned;
1997-10-15, by wenzelm
eliminated aliasing merge: now always extends;
1997-10-15, by wenzelm
tuned comment;
1997-10-15, by wenzelm
improved print_data;
1997-10-15, by wenzelm
tuned;
1997-10-15, by wenzelm
slightly changed interfaces for oracles;
1997-10-15, by wenzelm
Added ack to Mateja Jamnik.
1997-10-15, by nipkow
tuned;
1997-10-15, by wenzelm
tuned;
1997-10-14, by wenzelm
added additional generic data;
1997-10-14, by wenzelm
Sign.print_data;
1997-10-14, by wenzelm
added init_data, get_data, put_data;
1997-10-14, by wenzelm
added data.ML;
1997-10-14, by wenzelm
Arbitrarily typed data.
1997-10-14, by wenzelm
Patch to avoid simplification of ~EX to ALL~
1997-10-14, by paulson
Two lemmas are already in List.
1997-10-14, by nipkow
More lemmas, esp. ~Bex and ~Ball conversions.
1997-10-14, by nipkow
Added neagtion rules for Ball and Bex.
1997-10-14, by nipkow
tuned;
1997-10-14, by wenzelm