isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

catches exception DELETE
2003-04-26, by paulson
no need to be nice everywhere
2003-04-25, by kleing
Auth: certified email protocol
2003-04-25, by paulson
Changes required by the certified email protocol
2003-04-25, by paulson
Fixed problem in add_elim_realizer which caused bound variables to
2003-04-23, by berghofe
more documentation
2003-04-23, by kleing
Got rid of the [iff], which was effectively inserting converseD
2003-04-23, by paulson
Tuned realizer for exE rule, to avoid blowup of extracted program.
2003-04-23, by berghofe
elim_vars now handles both Vars and Frees.
2003-04-23, by berghofe
elim_cong now eta-expands proofs on the fly if required.
2003-04-23, by berghofe
Eliminated most occurrences of rule_format attribute.
2003-04-23, by berghofe
header
2003-04-16, by nipkow
Added take/dropWhile thms
2003-04-16, by nipkow
fixed document
2003-04-15, by kleing
added thm"..." due to new Map.thy
2003-04-14, by nipkow
Added thms
2003-04-14, by nipkow
Fixed non-escaped underscore in section headings (document generation should
2003-04-14, by webertj
Map.ML integrated into Map.thy
2003-04-11, by webertj
tidying
2003-04-09, by paulson
Removal of Summation theory
2003-04-09, by paulson
Fixed bug in adjustcoeffeq_wp.
2003-04-08, by berghofe
try_param_tac now precomputes substitution for rule, in order to avoid
2003-04-08, by berghofe
First working version
2003-04-08, by nipkow
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
2003-04-07, by nipkow
use 2 processors on sunbroy1
2003-04-06, by kleing
run on sunbroy1, too
2003-04-06, by kleing
*** empty log message ***
2003-04-06, by nipkow
Map.empty is now a translation
2003-04-05, by nipkow
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
removed since 1994 or earlier
2003-04-05, by kleing
Fixed bug in eta_long.
2003-04-04, by berghofe
type_of_G now applies type substitution before decomposing type.
2003-04-04, by berghofe
Made empty a translation rather than a constant.
2003-04-01, by nipkow
Fixed Coset.thy (proved theorem factorgroup_is_group).
2003-04-01, by ballarin
more comments and tweaks
2003-03-31, by paulson
tidied
2003-03-31, by paulson
Margin for pretty-printing is now a mutable reference.
2003-03-29, by berghofe
Proofs for section 4.5.3
2003-03-26, by paulson
Added show_brackets to settings menu.
2003-03-25, by berghofe
Re-structured some proofs in order to get rid of rule_format attribute.
2003-03-25, by berghofe
New theorems split_div' and mod_div_equality'.
2003-03-25, by berghofe
Presburger arithmetic
2003-03-25, by berghofe
Added examples for Presburger arithmetic.
2003-03-25, by berghofe
Added decision procedure for Presburger arithmetic.
2003-03-25, by berghofe
Added Presburger theory.
2003-03-25, by berghofe
Added hook for presburger arithmetic decision procedure.
2003-03-25, by berghofe
New decision procedure for Presburger arithmetic.
2003-03-25, by berghofe
*** empty log message ***
2003-03-23, by nipkow
More on progress sets
2003-03-21, by paulson
quadratic reciprocity files
2003-03-21, by paulson
Gauss, UNITY, ZF
2003-03-20, by paulson
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
2003-03-20, by paulson
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
2003-03-18, by paulson
toggled show_main_goal
2003-03-18, by nipkow
*** empty log message ***
2003-03-18, by nipkow
just a few mods to a few thms
2003-03-17, by nipkow
More "progress set" material
2003-03-17, by paulson

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle