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

1 -> 1'
2001-08-06, by nipkow
Changed 1 to 1' (= Suc 0)
2001-08-06, by paulson
turned translation for 1::nat into def.
2001-08-06, by nipkow
three new theorems
2001-08-06, by paulson
removed the warning from [iff]
2001-08-06, by paulson
removed an unsuitable default simprule
2001-08-06, by paulson
tidying and moving the theorem "choice"
2001-08-06, by paulson
new result comp_surj
2001-08-06, by paulson
numerous stylistic changes and indexing
2001-08-03, by paulson
additional revisions to chapters 1, 2
2001-07-26, by paulson
revisions and indexing
2001-07-26, by paulson
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some
2001-07-25, by paulson
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-07-25, by paulson
partial restructuring to reduce dependence on Axiom of Choice
2001-07-25, by paulson
removed reference to Ex_def
2001-07-25, by paulson
partial restructuring to reduce dependence on Axiom of Choice
2001-07-25, by paulson
tweaks and indexing
2001-07-24, by paulson
cosmetics
2001-07-23, by oheimb
Final version of Florian Kammueller's examples
2001-07-23, by paulson
new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-23, by paulson
improved version of the Pi-theorems
2001-07-23, by paulson
PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-23, by paulson
live links
2001-07-23, by paulson
The final version of Florian Kammueller's proofs
2001-07-23, by paulson
slight improvement for iff attribute
2001-07-23, by oheimb
replaced SOME by THE;
2001-07-22, by wenzelm
the_equality [intro];
2001-07-22, by wenzelm
tuned;
2001-07-22, by wenzelm
declare trans [trans] (*overridden in theory Calculation*);
2001-07-22, by wenzelm
HOL: added "The";
2001-07-20, by wenzelm
private "myinv" (uses "The" instead of "Eps");
2001-07-20, by wenzelm
replaced "Eps" by "The";
2001-07-20, by wenzelm
HOL_ss: the_eq_trivial, the_sym_eq_trivial;
2001-07-20, by wenzelm
tuned;
2001-07-20, by wenzelm
added "The" (definite description operator) (by Larry);
2001-07-20, by wenzelm
*** empty log message ***
2001-07-20, by wenzelm
SEDINDEX = ./isa-index;
2001-07-20, by wenzelm
tidying the index
2001-07-17, by paulson
tidying the index
2001-07-17, by paulson
indexing
2001-07-16, by paulson
abtract non-emptiness statements (no longer use Eps);
2001-07-15, by wenzelm
tuned;
2001-07-15, by wenzelm
working
2001-07-13, by paulson
oops
2001-07-13, by paulson
fixed bad error in tdxbold; also removed default indexing in \\rulename
2001-07-13, by paulson
tweaks
2001-07-13, by paulson
added\\protect
2001-07-13, by paulson
more indexing
2001-07-13, by paulson
indexing tweaks
2001-07-13, by paulson
less indexing of theorem names
2001-07-13, by paulson
indexing
2001-07-13, by paulson
contrapos_pn
2001-07-13, by paulson
index file
2001-07-13, by paulson
removed a4paper
2001-07-12, by paulson
more in the Springer style
2001-07-12, by paulson
indexing
2001-07-12, by paulson
indexing
2001-07-11, by paulson
messages, and proper treatment of footnotes
2001-07-11, by paulson
new preface
2001-07-11, by paulson
tweaks for new version
2001-07-11, by paulson
indexing and tweaks
2001-07-11, by paulson
tweak
2001-07-11, by paulson
careful changes to make its output identical to that of indexing macros
2001-07-11, by paulson
new macro file for the tutorial
2001-07-11, by paulson
separate preface and macro file
2001-07-11, by paulson
do not remove Rules and Sets TeX files
2001-07-11, by paulson
isa-index replaces ../sedindex: knows about \\isa
2001-07-09, by paulson
two Isar tactic scripts
2001-07-06, by paulson
Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
2001-07-03, by wenzelm
GroupTheory
2001-07-03, by paulson
new lemmas
2001-07-03, by paulson
better treatment of restrict (lam)
2001-07-03, by paulson
Locale-based group theory proofs
2001-07-03, by paulson
ppc-darwin;
2001-07-02, by wenzelm
do *not* ./configure;
2001-07-02, by wenzelm
#!/usr/bin/env bash;
2001-07-02, by wenzelm
...
2001-07-02, by wenzelm
the records section
2001-06-29, by paulson
the records section
2001-06-29, by paulson
for the records section
2001-06-29, by paulson
a few new and/or improved results
2001-06-26, by paulson
gave Greatest_le its proper name
2001-06-26, by paulson
resolved name clash
2001-06-26, by paulson
tidied
2001-06-26, by paulson
now more like the HOL versions, and with the Square Root example added
2001-06-26, by paulson
tidying and consolidating files
2001-06-26, by paulson
tidying and consolidating files
2001-06-26, by paulson
removed duplicate proof and small mod.
2001-06-26, by nipkow
Simprocs for type "nat" no longer introduce numerals unless
2001-06-25, by paulson
Simprocs for type "nat" no longer introduce numerals unless they are already
2001-06-25, by paulson
added NanoJava
2001-06-16, by oheimb
tidied
2001-06-13, by paulson
New proof of gcd_zero after a change to Divides.ML made the old one fail
2001-06-13, by paulson
a couple of new theorems
2001-06-13, by paulson
corrected xsymbol/HTML syntax
2001-06-12, by oheimb
Fixed bug in function rebuild.
2001-06-11, by berghofe
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
2001-06-10, by paulson
tuned
2001-06-09, by wenzelm
tuned Primes theory;
2001-06-09, by wenzelm
addition of the GREATEST quantifier
2001-06-09, by paulson
renaming of evs in the Fake rule
2001-06-09, by paulson
new material from the Sylow proof
2001-06-09, by paulson
simplified a proof using new dvd rules
2001-06-09, by paulson
moved Primes.thy from NumberTheory to Library
2001-06-09, by paulson
Removed BCV
2001-06-08, by nipkow
*** empty log message ***
2001-06-05, by nipkow
This is now superseded by MicroJava/BV
2001-06-05, by nipkow
renamed # to ## to avoid clashing with List cons
2001-06-01, by paulson
now checks for leading meta-quantifiers and complains, instead of
2001-06-01, by paulson
tuned
2001-05-31, by wenzelm
added HOL-CTL;
2001-05-31, by wenzelm
tuned
2001-05-31, by wenzelm
examples files start from Main instead of various ZF theories
2001-05-31, by paulson
invent_names
2001-05-31, by wenzelm
added HOL-CTL example;
2001-05-31, by bauerg
added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-31, by oheimb
added FOCUS including the One-Element Buffer by Manfred Broy
2001-05-31, by oheimb
added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-31, by oheimb
added stream length, map, and filter
2001-05-31, by oheimb
corrected ML names of definitions, added chain_shift
2001-05-31, by oheimb