Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+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.
renamed forall_elim_vars_safe to gen_all;
2002-01-12, by wenzelm
Isabelle2002 (January 2002);
2002-01-11, by wenzelm
removed obsolete isamode.ML;
2002-01-11, by wenzelm
tuned;
2002-01-11, by wenzelm
#!/usr/bin/env bash;
2002-01-11, by wenzelm
replace gen_all by forall_elim_vars_safe;
2002-01-11, by wenzelm
improved forall_elim_vars_safe (no longer invents new indexes);
2002-01-11, by wenzelm
lemmas (in ACe) AC;
2002-01-11, by wenzelm
tuned;
2002-01-11, by wenzelm
IsarThy.theorems_i;
2002-01-11, by wenzelm
moved setmksimps to Main!
2002-01-11, by wenzelm
have_thmss vs. have_thmss_i;
2002-01-11, by wenzelm
clarified/added theorems(_i) vs. locale_theorems(_i);
2002-01-11, by wenzelm
localized 'lemmas', 'theorems', 'declare';
2002-01-11, by wenzelm
have_thmss vs. have_thmss_i;
2002-01-11, by wenzelm
kind: ignore "";
2002-01-11, by wenzelm
IsarThy.theorems_i;
2002-01-11, by wenzelm
clarified IsarThy.apply_theorems_i;
2002-01-11, by wenzelm
* Pure: localized 'lemmas', 'theorems', 'declare';
2002-01-11, by wenzelm
removed add_thmss;
2002-01-10, by wenzelm
tuned;
2002-01-10, by wenzelm
export_single;
2002-01-10, by wenzelm
refine_tac: Tactic.norm_hhf_tac before trying rule;
2002-01-10, by wenzelm
add_thmss_hybrid;
2002-01-10, by wenzelm
export multi_theorem(_i), locale_multi_theorem(_i);
2002-01-10, by wenzelm
stylistic changes
2002-01-10, by paulson
*** empty log message ***
2002-01-10, by nipkow
locales: hide base name of exported version;
2002-01-10, by wenzelm
simplified theorem(_i);
2002-01-10, by wenzelm
IsarThy.smart_multi_theorem;
2002-01-10, by wenzelm
added hide_thms;
2002-01-10, by wenzelm
simplified IsarThy.theorem_i;
2002-01-10, by wenzelm
qualified exports from locales;
2002-01-10, by wenzelm
obsolete;
2002-01-09, by wenzelm
converted theory Transitive_Closure;
2002-01-09, by wenzelm
* added \<euro> symbol;
2002-01-09, by wenzelm
no longer requires TEXINPUTS;
2002-01-09, by wenzelm
isatool latex -o sty;
2002-01-09, by wenzelm
removed TEXINPUTS;
2002-01-09, by wenzelm
updated;
2002-01-09, by wenzelm
tuned;
2002-01-09, by wenzelm
updated;
2002-01-09, by wenzelm
tuned;
2002-01-09, by wenzelm
updated;
2002-01-09, by wenzelm
tuned;
2002-01-09, by wenzelm
tuned message;
2002-01-09, by wenzelm
changed the index sort key from |-| to just |- because pdflatex can't cope
2002-01-09, by paulson
HOL-Hyperreal produces an image (again);
2002-01-08, by wenzelm
dependencies for "typedef" image;
2002-01-08, by wenzelm
improved arrangement of "typedef" images;
2002-01-08, by wenzelm
no_document use_thy "While_Combinator";
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
updated;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
\part{Elementary Techniques};
2002-01-08, by wenzelm
\chapter{The Basics};
2002-01-08, by wenzelm
Added some simprules proofs.
2002-01-08, by paulson
updated;
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
added filter_filter
2002-01-08, by nipkow
#2 to 2
2002-01-08, by paulson
syntax "_not_equal";
2002-01-08, by wenzelm
removed (not really necessary, causes too many consistency problems);
2002-01-08, by wenzelm
tuned;
2002-01-08, by wenzelm
getting close to completion;
2002-01-07, by wenzelm
updated;
2002-01-07, by wenzelm
tuned;
2002-01-07, by wenzelm
updated;
2002-01-07, by wenzelm
tuned;
2002-01-07, by wenzelm
tuned deps;
2002-01-07, by wenzelm
tuned;
2002-01-07, by wenzelm
updated;
2002-01-07, by wenzelm
some more ...;
2002-01-06, by wenzelm
"_not_equal" dummy constant;
2002-01-06, by wenzelm
updated;
2002-01-06, by wenzelm
some more text;
2002-01-06, by wenzelm
updated;
2002-01-06, by wenzelm
tuned;
2002-01-06, by wenzelm
some text on document preparation;
2002-01-05, by wenzelm
updated;
2002-01-05, by wenzelm
tuned;
2002-01-05, by wenzelm
updated;
2002-01-05, by wenzelm
mention X-Symbol;
2002-01-05, by wenzelm
updated;
2002-01-05, by wenzelm
use wasysym package;
2002-01-05, by wenzelm
\newcommand{\isasymignore}{}, so we may use \<ignore> to disambiguate
2002-01-05, by wenzelm
tuned;
2002-01-05, by wenzelm
\hfootref: use \url markup;
2002-01-05, by wenzelm
more on concrete syntax;
2002-01-05, by wenzelm
fixed \index;
2002-01-05, by wenzelm
tuned ``syntax (output)'';
2002-01-04, by wenzelm
isatool document: stderr to stdout;
2002-01-04, by wenzelm
tuned;
2002-01-04, by wenzelm
document preparation overview;
2002-01-04, by wenzelm
beginnings of concrete syntax;
2002-01-04, by wenzelm
include typedef image without path prefix!
2002-01-04, by wenzelm
updated;
2002-01-04, by wenzelm
link Types/typedef images;
2002-01-04, by wenzelm
Isar version;
2002-01-03, by wenzelm
tuned msg;
2002-01-03, by wenzelm
\CONSTDEFS;
2002-01-03, by wenzelm
tuned;
2002-01-03, by wenzelm
next round of updates;
2002-01-03, by wenzelm
Some new theorems for ordinals
2002-01-03, by paulson
tuned;
2002-01-02, by wenzelm
first stage of major update;
2002-01-02, by wenzelm
added zf.tex;
2002-01-02, by wenzelm
added isabelle-intro, isabelle-logics;
2002-01-02, by wenzelm
added \indexisarcmdof, \indexisarmethof, \indexisarattof;
2002-01-02, by wenzelm
New theorems by Sidi Ehmety
2002-01-02, by paulson
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
2002-01-02, by paulson
Added "Executing higher order logic" paper.
2001-12-31, by berghofe
Added section on code generator.
2001-12-31, by berghofe
tuned document sources;
2001-12-29, by wenzelm
'inductive_cases': support 'and' form;
2001-12-29, by wenzelm
* ZF/IMP: updated and converted to new-style theory format;
2001-12-29, by wenzelm
update by Stephan Merz;
2001-12-29, by wenzelm
conversion to Isar/ZF
2001-12-28, by paulson
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip