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

include more explanation of variables
2004-03-09, by kleing
*** empty log message ***
2004-03-08, by ballarin
Bug-fixes for transitivity reasoner.
2004-03-08, by ballarin
Added documentation for transitivity solver setup.
2004-03-08, by ballarin
generic theorems about exponentials; general tidying up
2004-03-08, by paulson
new theory of infinite sets
2004-03-08, by paulson
Lex: removed last ML files
2004-03-06, by nipkow
Conversion ML -> Isar
2004-03-06, by nipkow
tweaked for times_ac1
2004-03-05, by paulson
tweaks
2004-03-05, by paulson
some new results
2004-03-05, by paulson
some new results
2004-03-05, by paulson
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
2004-03-05, by paulson
patch to NumberTheory problems caused by Parity
2004-03-05, by paulson
do not remove heaps, used for afp test
2004-03-05, by kleing
Lex: ML -> thy
2004-03-04, by nipkow
ML -> Isar
2004-03-04, by nipkow
new material from Avigad, and simplified treatment of division by 0
2004-03-04, by paulson
Removed ML files from Lex
2004-03-04, by nipkow
Conversion of ML files to Isar.
2004-03-04, by nipkow
added record_ex_sel_eq_simproc
2004-03-03, by schirmer
fixed bugs in the setup of arithmetic procedures
2004-03-02, by paulson
converted Hyperreal/IntFloor to Isar script
2004-03-02, by paulson
tuned. proofs still gruesome..
2004-03-02, by kleing
converted MiniML to Isar
2004-03-02, by kleing
converted to Isar
2004-03-02, by kleing
new Ring_and_Field hierarchy, eliminating redundant axioms
2004-03-01, by paulson
converted Hyperreal/HTranscendental to Isar script
2004-03-01, by paulson
converted to Isar
2004-03-01, by kleing
union/intersection over intervals
2004-03-01, by kleing
Added specific code generator for number_of.
2004-02-29, by berghofe
converted Hyperreal/Series to Isar script
2004-02-26, by paulson
converted Hyperreal/NatStar to Isar script
2004-02-26, by paulson
corrected authors
2004-02-26, by nipkow
converted Hyperreal/HSeries to Isar script
2004-02-25, by paulson
find_tname now handles parameter renaming properly ("as they are printed").
2004-02-25, by berghofe
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
2004-02-24, by paulson
converted NSCA to Isar script
2004-02-24, by paulson
converted HOL/Complex/NSInduct to Isar script
2004-02-23, by paulson
converted HOL/Complex/NSCA to Isar script
2004-02-23, by paulson
conversion of Complex/CStar to Isar script
2004-02-21, by paulson
conversion of Complex/CSeries to Isar script
2004-02-21, by paulson
conversion of Complex/CLim to Isar script
2004-02-21, by paulson
Transitive_Closure: added consumes and case_names attributes
2004-02-21, by nipkow
new "where" section
2004-02-20, by paulson
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
2004-02-20, by nipkow
removal of the legacy ML structure List
2004-02-19, by paulson
new numerics section using type classes
2004-02-19, by paulson
New lemmas about inversion of restricted functions.
2004-02-19, by ballarin
Efficient, graph-based reasoner for linear and partial orders.
2004-02-19, by ballarin
moved list_all2I to List.thy
2004-02-19, by paulson
removed a reference to the ML structure List.thy
2004-02-19, by paulson
new theorem
2004-02-19, by paulson
comments!!
2004-02-19, by paulson
new Union syntax
2004-02-18, by paulson
removed obsolete theorem
2004-02-18, by paulson
Moved application of flexflex_unique from standard' to standard.
2004-02-17, by berghofe
further tweaks to the numeric theories
2004-02-17, by paulson
arith
2004-02-16, by paulson
lemmas about card (set xs)
2004-02-16, by kleing
Polymorphic treatment of binary arithmetic using axclasses
2004-02-15, by paulson
Removed dangling exception handler
2004-02-14, by nipkow
Missing } inserted
2004-02-12, by nipkow
Removed "duplicate fact binding" error message.
2004-02-11, by berghofe
Printing functions now use cond_extrn instead of extrn
2004-02-11, by berghofe
Added flag short_names
2004-02-11, by berghofe
Modified UN and INT xsymbol syntax: made index subscript
2004-02-11, by nipkow
*** empty log message ***
2004-02-11, by nipkow
updated links to the old ftp site
2004-02-10, by paulson
generic of_nat and of_int functions, and generalization of iszero
2004-02-10, by paulson
tidying up, especially the Complex numbers
2004-02-05, by paulson
Changed variable names.
2004-02-05, by nipkow
*** empty log message ***
2004-02-04, by nipkow
further tidying of the complex numbers
2004-02-03, by paulson
tidying of the complex numbers
2004-02-03, by paulson
Finally fixed the counterexample finder. Can now deal with < on real.
2004-02-03, by nipkow
Conversion of HyperNat to Isar format and its declaration as a semiring
2004-02-02, by paulson
simplifications in the hyperreals
2004-01-29, by paulson
tidying up arithmetic for the hyperreals
2004-01-28, by paulson
converted Real/Lubs to Isar script. Converting arithmetic setup
2004-01-28, by paulson
remove more files (index, log files) for -c option
2004-01-28, by kleing
replacing HOL/Real/PRat, PNat by the rational number development
2004-01-27, by paulson
replacing HOL/Real/PRat, PNat by the rational number development
2004-01-27, by paulson
\<^raw...> does no longer print an additional space.
2004-01-27, by schirmer
Reduced space for xsymbols output of [| |] ==> from 3 to 1
2004-01-27, by nipkow
\\<...> will be converted to \<...>
2004-01-26, by schirmer
* Support for raw latex output in control symbols: \<^raw...>
2004-01-26, by schirmer
Added an exception handler and error msg.
2004-01-25, by nipkow
Added print translation for pairs
2004-01-20, by schirmer
cleaning up
2004-01-20, by schirmer
print translation for ALL x <= n. P x
2004-01-14, by kleing
fixed old bugs in "decomp" (conversion from term to lin.arith. format).
2004-01-14, by nipkow
Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-14, by nipkow
types complex and hcomplex are now instances of class ringpower:
2004-01-13, by paulson
Added lemmas to Ring_and_Field with slightly modified simplification rules
2004-01-12, by paulson
Modified real arithmetic simplification
2004-01-12, by paulson
Fixed compatibility issues with SML/NJ:
2004-01-12, by webertj
Adding 'refute' to HOL.
2004-01-10, by webertj
'refute', 'refute_params'.
2004-01-10, by webertj
Defining the type class "ringpower" and deleting superseded theorems for
2004-01-09, by paulson
set isasep to {} by default
2004-01-09, by kleing
Added lazy sequences and parser combinators for same.
2004-01-08, by skalberg
separate thm lists in latex output by \isasep
2004-01-08, by kleing
run makeindex if necessary
2004-01-08, by kleing
map_idI
2004-01-07, by kleing
auto update
2004-01-06, by paulson
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
2004-01-06, by paulson
correction to cterm_instantiate by Christoph Leuth
2004-01-06, by paulson
*** empty log message ***
2004-01-05, by nipkow
*** empty log message ***
2004-01-05, by nipkow
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
2004-01-05, by nipkow
Deleting more redundant theorems
2004-01-03, by paulson
conversion of Real/PReal to Isar script;
2004-01-01, by paulson
tweaking of lemmas in RealDef, RealOrd
2004-01-01, by paulson
\<^bsub> .. \<^esub>
2003-12-29, by kleing
spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup>
2003-12-29, by kleing
re-organized numeric lemmas
2003-12-27, by paulson
Added trace msg
2003-12-25, by nipkow
re-organized some hyperreal and real lemmas
2003-12-25, by paulson
list_all2_nthD no good as [intro?]
2003-12-24, by kleing