Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-300
-100
-96
+96
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
removed smlnj-1.07;
1997-08-05, by wenzelm
cleaned up;
1997-08-05, by wenzelm
tuned comments;
1997-08-05, by wenzelm
removed ML-Systems/smlnj-1.07.ML;
1997-08-05, by wenzelm
SML/NJ 1.07 no longer supported!
1997-08-05, by wenzelm
cleaned up;
1997-08-05, by wenzelm
Added example mapf which requires a special congruence rule.
1997-08-05, by nipkow
Added function `replicate' and lemmas map_cong and set_replicate.
1997-08-05, by nipkow
cleaned up;
1997-08-05, by wenzelm
Corrected a comment
1997-08-05, by paulson
Added a take/dropWhile lemma.
1997-08-04, by nipkow
Generalized nth_drop (Conny).
1997-08-01, by nipkow
Corected bug in def of dropWhile (also present in Haskell lib!)
1997-08-01, by nipkow
Had to remove {x.x=a} = a from !simpset in one proof.
1997-08-01, by nipkow
Added {x.x=a} = a to !simpset.
1997-08-01, by nipkow
removed split_paired_Ex;
1997-07-25, by wenzelm
new simproc
1997-07-25, by nipkow
*** empty log message ***
1997-07-25, by wenzelm
load simplifier.ML (again);
1997-07-25, by wenzelm
added prems argument to simplification procedures;
1997-07-25, by wenzelm
remove references to simplifier.ML;
1997-07-25, by wenzelm
improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-25, by wenzelm
Added a few lemmas.
1997-07-24, by nipkow
Deleted comment.
1997-07-24, by nipkow
Replaced clumsy rewriting by the new function simplify on thms.
1997-07-24, by nipkow
List.ML: added lemmas by Stefan Merz.
1997-07-24, by nipkow
set_of_list -> set
1997-07-24, by paulson
Simplified a few proofs because of improved simplification.
1997-07-23, by nipkow
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
1997-07-23, by nipkow
added simplification meta rules;
1997-07-23, by wenzelm
standard congs;
1997-07-23, by wenzelm
Now rename_params_rule merely issues warnings--and does nothing--if the
1997-07-23, by paulson
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
1997-07-23, by paulson
Uses new version of Datatype.occs_in_prems
1997-07-23, by paulson
auto update
1997-07-23, by paulson
Removal of tactical STATE
1997-07-23, by paulson
fixed polymorphic val;
1997-07-23, by wenzelm
tuned congs: standard;
1997-07-23, by wenzelm
improved simp tracing;
1997-07-23, by wenzelm
added simplification meta rules;
1997-07-23, by wenzelm
tmp fix to accomodate rep_ss changes;
1997-07-23, by wenzelm
added rewrite_thm;
1997-07-23, by wenzelm
tuned apsome;
1997-07-23, by wenzelm
added error_msg;
1997-07-22, by wenzelm
tuned error / warning;
1997-07-22, by wenzelm
added print_ss;
1997-07-22, by wenzelm
added dest_mss, merge_mss;
1997-07-22, by wenzelm
tuned title;
1997-07-22, by wenzelm
added dest and merge operations;
1997-07-22, by wenzelm
added pretty_cterm;
1997-07-22, by wenzelm
improved print_cs;
1997-07-22, by wenzelm
Cosmetic changes: margins, indentation, ...
1997-07-22, by paulson
Now possibility_tac is an explicit function, in order to delay
1997-07-22, by paulson
Cosmetic changes: margins, indentation, ...
1997-07-22, by paulson
Now possibility_tac and basic_possibility_tac are explicit functions, in order
1997-07-22, by paulson
Deleted the superfluous assumption A ~= B, which must hold anyway by induction
1997-07-22, by paulson
Fixed the spelling of AUTH_NAMES--it could not have worked before\!
1997-07-22, by paulson
Option is a synonym for General because MLWorks does not yet provide
1997-07-22, by paulson
Removal of the tactical STATE
1997-07-22, by paulson
Removal of the tactical STATE
1997-07-22, by paulson
tuned error propagation msg;
1997-07-18, by wenzelm
defs may now be conditional;
1997-07-18, by wenzelm
renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
tuned warnings;
1997-07-18, by wenzelm
considered removal of print_goals_ref;
1997-07-18, by wenzelm
defs: allow conditions;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
improved output channels: normal, warning, error;
1997-07-18, by wenzelm
fixed EqI meta rule;
1997-07-17, by wenzelm
changes needed for introducing fairness
1997-07-17, by mueller
changes neede for introducing fairness
1997-07-17, by mueller
changes needed for adding fairness
1997-07-17, by mueller
fixed merge of internal simprocs;
1997-07-16, by wenzelm
Changing "lost" from a parameter of protocol definitions to a constant.
1997-07-14, by paulson
Fixed delIffs to deal correctly with the D-rule
1997-07-14, by paulson
Removed redundant addsimps of Un_insert_left, which is now a default simprule
1997-07-14, by paulson
Removal of monotonicity reasoning involving "lost" and the theorem
1997-07-11, by paulson
Now uses the Notes constructor to distinguish the Client (who has chosen M)
1997-07-11, by paulson
Moved some declarations to Message from Public and Shared
1997-07-11, by paulson
Now loads theory Event, which contains common declarations
1997-07-11, by paulson
Moving common declarations and proofs from theories "Shared"
1997-07-11, by paulson
removed obsolete init_pps and init_thy_reader;
1997-07-09, by wenzelm
improved type checking errors;
1997-07-09, by wenzelm
removed init_pps;
1997-07-09, by wenzelm
removed init_database;
1997-07-09, by wenzelm
Improved length = size translation.
1997-07-09, by nipkow
New proofs involving CERTIFICATE VERIFY
1997-07-07, by paulson
eliminated chmod -w;
1997-07-07, by wenzelm
-w option;
1997-07-07, by wenzelm
NOWRITE;
1997-07-07, by wenzelm
added -w option;
1997-07-07, by wenzelm
Changed some variables of type msg to lower case (e.g. from NB to nb
1997-07-04, by paulson
less
more
|
(0)
-3000
-1000
-300
-100
-96
+96
+100
+300
+1000
+3000
+10000
+30000
tip