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

* HOL: syntax translations now work properly with numerals and records
2001-08-08, by wenzelm
layout, subscripts
2001-08-08, by oheimb
[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";
2001-08-08, by wenzelm
polyml-4.1.1;
2001-08-08, by wenzelm
Hilbert_Choice is needed only in Main itself
2001-08-08, by paulson
Main is the proper parent of IOA
2001-08-08, by paulson
get it working again using Hilbert_Choice
2001-08-08, by paulson
Getting it working again with 1' instead of 1
2001-08-08, by paulson
new ZF/UNITY theory
2001-08-08, by paulson
*** empty log message ***
2001-08-08, by wenzelm
changed to full expressions with side effects
2001-08-08, by oheimb
changed to full expressions with side effects
2001-08-08, by oheimb
tuned;
2001-08-07, by wenzelm
tuned;
2001-08-07, by wenzelm
fix problem with user translations by making field names appear as consts;
2001-08-07, by wenzelm
tuned;
2001-08-07, by wenzelm
- Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
2001-08-07, by berghofe
Eliminated dependency of Funs_rangeE on SOME.
2001-08-07, by berghofe
removed the warning from [iff]
2001-08-07, by oheimb
Tweaks for 1 -> 1'
2001-08-07, by paulson
Converted 1 to 1'
2001-08-06, by paulson
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