Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-112
+112
+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.
AddIffs[not_None_eq];
1998-09-09, by oheimb
AddSDs[override_SomeD];
1998-09-09, by oheimb
changed constants mem and list_all to mere translations
1998-09-09, by oheimb
changed order of included theories
1998-09-09, by oheimb
added Id_apply
1998-09-09, by oheimb
removed superfluous AddIs thms (were already in)
1998-09-09, by oheimb
renamed sswhen to sscase
1998-09-09, by oheimb
simplified definition of axclass cpo
1998-09-09, by oheimb
added caveat; a real solution would be difficult
1998-09-08, by oheimb
improved spacing
1998-09-08, by oheimb
adapted modifiers: Mod1 -> Mod2, Mod5 -> Mod4
1998-09-08, by oheimb
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
1998-09-08, by paulson
Got rid of not_Says_to_self; re-organized proofs
1998-09-08, by paulson
new example; tidying
1998-09-07, by paulson
new example
1998-09-07, by paulson
New UNITY theory, the N-S protocol
1998-09-07, by paulson
tidying
1998-09-07, by paulson
Function 'upt'
1998-09-04, by nipkow
Arith: less_diff_conv
1998-09-04, by nipkow
A new approach, using simp_of_act and simp_of_set to activate definitions when
1998-09-03, by paulson
Added function upto to List.
1998-09-02, by nipkow
modified proofs for new constrains_tac and ensures_tac
1998-09-02, by paulson
two new thms
1998-09-02, by paulson
Moved constrains_tac from SubstAx to Constrains.
1998-09-02, by paulson
small simplification to not_Says_to_self
1998-09-02, by paulson
New approach, using a locale
1998-09-01, by paulson
tidied
1998-09-01, by paulson
Replaced Suc_diff_n by Suc_diff_le
1998-09-01, by paulson
new theory Induct/FoldSet
1998-09-01, by paulson
New law card_Un_Int. Removed card_insert from simpset
1998-09-01, by paulson
tidying; moved diff_less to Arith.ML
1998-09-01, by paulson
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
1998-09-01, by paulson
New lemmas involving Int
1998-09-01, by paulson
New lemmas involving Int
1998-09-01, by paulson
fixed error msg
1998-09-01, by paulson
Moved lemmas to Arith.ML
1998-09-01, by paulson
Two new subtraction lemmas
1998-09-01, by paulson
made SML/NJ happy;
1998-08-30, by wenzelm
* print mode 'emacs' reserved for Isamode;
1998-08-28, by wenzelm
added emacs mode;
1998-08-28, by wenzelm
tuned isatool install;
1998-08-28, by wenzelm
tuned;
1998-08-28, by wenzelm
-d DISTDIR;
1998-08-28, by wenzelm
tuned;
1998-08-28, by wenzelm
www.in.tum.de;
1998-08-27, by wenzelm
made tutorial first;
1998-08-27, by wenzelm
tuned;
1998-08-27, by wenzelm
exec;
1998-08-27, by wenzelm
* Pure: ML function 'theory_of' replaced by 'theory';
1998-08-27, by wenzelm
tuned;
1998-08-27, by wenzelm
isatool install;
1998-08-27, by wenzelm
added tutorial;
1998-08-27, by wenzelm
fixed ISABELLE_USEDIR_OPTIONS;
1998-08-27, by wenzelm
*** empty log message ***
1998-08-27, by wenzelm
Goal, Goalw;
1998-08-27, by wenzelm
moeved get_thm etc. to goals.tex;
1998-08-27, by wenzelm
tuned doc name;
1998-08-27, by wenzelm
fixed center;
1998-08-27, by wenzelm
ISABELLE_USEDIR_OPTIONS="-i false";
1998-08-27, by wenzelm
tuned;
1998-08-27, by wenzelm
eps logis;
1998-08-27, by wenzelm
href eps versions;
1998-08-27, by wenzelm
weblinted, tuned;
1998-08-27, by wenzelm
fake proper eps header;
1998-08-27, by wenzelm
fixed tutorial;
1998-08-26, by wenzelm
added HOL tutorial;
1998-08-26, by wenzelm
added HOL tutorial;
1998-08-26, by wenzelm
junk
1998-08-26, by nipkow
*** empty log message ***
1998-08-26, by nipkow
*** empty log message ***
1998-08-26, by nipkow
The HOL tutorial.
1998-08-26, by nipkow
moved images to gfx dir;
1998-08-26, by wenzelm
tuned;
1998-08-24, by wenzelm
SYNC;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
added nonterminals, setup;
1998-08-24, by wenzelm
added Antiquote example;
1998-08-24, by wenzelm
mkdir -p;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
SYNC;
1998-08-24, by wenzelm
emacs local vars;
1998-08-24, by wenzelm
isatool install;
1998-08-24, by wenzelm
install binaries with absolute references to ISABELLE_HOME/bin;
1998-08-24, by wenzelm
debugged split_eta_proc
1998-08-24, by oheimb
tidied
1998-08-21, by paulson
Tidying
1998-08-21, by paulson
New UNITY files
1998-08-21, by paulson
New theory Lift
1998-08-20, by paulson
new theorems
1998-08-20, by paulson
tidied
1998-08-20, by paulson
new theorems; adds [le_refl, less_imp_le] as simprules
1998-08-20, by paulson
adjusted for new rewrites
1998-08-20, by paulson
tidied
1998-08-20, by paulson
tidied
1998-08-20, by paulson
Must remove leD from simpset
1998-08-20, by paulson
tidied
1998-08-20, by paulson
Must remove less_imp_le from simpset
1998-08-20, by paulson
Added converse_rtranclE(2)
1998-08-20, by nipkow
Now qed_spec_mp respects locales, by calling ml_store_thm
1998-08-20, by paulson
fixed param;
1998-08-19, by wenzelm
assume: adjust_maxidx;
1998-08-19, by wenzelm
new version, more resistant to PROOF FAILED. Now it distinguishes between
1998-08-19, by paulson
The warning "Rewrite rule from different theory" is ALWAYS printed, even if
1998-08-19, by paulson
new theorem zero_less_diff
1998-08-19, by paulson
Misc changes
1998-08-19, by paulson
Deleted obsolete declaration of PartE'
1998-08-19, by paulson
Tidied, removing uses of less_imp_diff_positive
1998-08-19, by paulson
tidied
1998-08-19, by paulson
fixed overloading of "image"
1998-08-19, by paulson
Overloading decl should assist Blast_tac
1998-08-19, by paulson
less_imp_diff_positive is redundant with new simprule zero_less_diff
1998-08-19, by paulson
less
more
|
(0)
-3000
-1000
-112
+112
+1000
+3000
+10000
+30000
tip