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

Greatly extended CRing. Added Module.
2003-04-30, by ballarin
tweaks
2003-04-29, by paulson
better guarantees
2003-04-29, by paulson
in \isanewline: \\ -> \par
2003-04-28, by kleing
Simplifier no longer aborts on failed congruence proof.
2003-04-28, by ballarin
Converted main proof to Isar.
2003-04-28, by berghofe
Converted main proofs to Isar.
2003-04-28, by berghofe
Added "break" flag to allow line breaks within \isa{...}
2003-04-28, by berghofe
Fixed problem in add_elim_realizer (concerning inductive predicates with
2003-04-27, by berghofe
converting more HOL-Auth to new-style theories
2003-04-26, by paulson
converting more HOL-Auth to new-style theories
2003-04-26, by paulson
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
moved one proof, added another
2003-03-17, by paulson
Bugs fixed and operators finprod and finsum.
2003-03-14, by ballarin
more about list_all2
2003-03-14, by kleing
fix for changes in HOL/Hoare/
2003-03-14, by kleing
Proved the main lemma on progress sets
2003-03-14, by paulson
new UN/INT simprules
2003-03-14, by paulson
split_name no longer uses Sign.string_of_typ to encode types, since
2003-03-13, by berghofe
*** empty log message ***
2003-03-11, by nipkow
*** empty log message ***
2003-03-11, by nipkow
*** empty log message ***
2003-03-11, by nipkow
addsplits / delsplits no longer ignore type of constant.
2003-03-11, by berghofe
First distributed version of Group and Ring theory.
2003-03-10, by ballarin
New theory ProgressSets. Definition of closure sets
2003-03-10, by paulson
spelling
2003-03-10, by paulson
new UNITY examples theory
2003-03-06, by paulson
new logical equivalences
2003-03-06, by paulson
new simprule for int (nat n)
2003-03-06, by paulson
link to devel snapshot
2003-03-06, by kleing
obsolete
2003-03-06, by kleing
new examples theory
2003-03-05, by paulson
get cvs to change modified time for session.tex
2003-03-02, by kleing
typo
2003-03-01, by kleing
added exercises
2003-03-01, by kleing
added Exercises
2003-03-01, by kleing
keep a copy of generated files in repository
2003-03-01, by kleing
keep a copy of generated files in repository
2003-03-01, by kleing
generate nightly devel snapshot
2003-02-28, by isatest
case distinction on host for makefile flags
2003-02-28, by isatest
Reorganized, moving many results about the integer dvd relation from IntPrimes
2003-02-27, by paulson
restored some deleted lemmas
2003-02-27, by paulson
Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-27, by ballarin
== -> =
2003-02-26, by kleing
zprime_def fixes by Jeremy Avigad
2003-02-26, by paulson
completed proofs for programs consisting of a single assignment
2003-02-26, by paulson
new lemma
2003-02-26, by paulson
some x-symbols and some new lemmas
2003-02-26, by paulson
*** empty log message ***
2003-02-25, by nipkow
added simp_depth_limit
2003-02-25, by nipkow
Documented prf / full_prf commands and antiquotations.
2003-02-25, by berghofe
Undid eta change for UN/INT.
2003-02-25, by nipkow
new inverse image lemmas
2003-02-20, by paulson
minor updates to pre-2002 release
2003-02-20, by paulson
fixed anomalies in the installed classical rules
2003-02-19, by paulson
check maxs in defensive machine
2003-02-18, by kleing
new theory Transformers: Meier-Sanders non-interference theory
2003-02-18, by paulson
Proof of the Schorr-Waite graph marking algorithm.
2003-02-17, by mehta
minor revisions
2003-02-16, by paulson
new theorem Compl_partition2
2003-02-16, by paulson
Product operator added --- preliminary.
2003-02-14, by ballarin