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

tuned headers -- adapted to usual conventions;
2007-05-31, by wenzelm
moved Compute_Oracle from Pure/Tools to Tools;
2007-05-31, by wenzelm
proper theory setup for compute oracle (based on CPure);
2007-05-31, by wenzelm
moved IsaPlanner from Provers to Tools;
2007-05-31, by wenzelm
moved IsaPlanner from Provers to Tools;
2007-05-31, by wenzelm
made aconvc pervasive;
2007-05-31, by wenzelm
moved aconvc to more_thm.ML;
2007-05-31, by wenzelm
tuned ML setup;
2007-05-31, by wenzelm
decode_term: force qualified name into Const;
2007-05-31, by wenzelm
proper loading of ML files (in HOL.thy);
2007-05-31, by wenzelm
HOL_proofs;
2007-05-31, by wenzelm
moved Integ files to canonical place;
2007-05-31, by wenzelm
proper loading of ML files;
2007-05-31, by wenzelm
removed dead code;
2007-05-31, by wenzelm
tuned header;
2007-05-31, by wenzelm
doc: exclude isabelle_isar.pdf;
2007-05-31, by wenzelm
tuned the proof
2007-05-31, by urbanc
introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-31, by urbanc
proper loading of ML files;
2007-05-31, by wenzelm
removed obsolete IFOL.thy/FOL.thy values;
2007-05-31, by wenzelm
proper loading of ML files;
2007-05-31, by wenzelm
tuned header;
2007-05-31, by wenzelm
tuned oracle setup;
2007-05-31, by wenzelm
moved HOLCF tools to canonical place;
2007-05-31, by wenzelm
moved TFL files to canonical place;
2007-05-31, by wenzelm
moved TFL files to canonical place;
2007-05-31, by wenzelm
added src/Tools;
2007-05-31, by wenzelm
fixed title;
2007-05-31, by wenzelm
Tools: generic tools outside of Pure.
2007-05-31, by wenzelm
moved Integ files to canonical place;
2007-05-31, by wenzelm
fixed use_thy "LocalWeakening";
2007-05-31, by wenzelm
included new example in the compiling process
2007-05-31, by urbanc
a theory using locally nameless terms and strong induction principles
2007-05-31, by urbanc
tuned the proof
2007-05-31, by urbanc
emulate later version of TextIO.inputLine;
2007-05-31, by wenzelm
reversed SML B library patches;
2007-05-31, by wenzelm
TextIO.inputLine: use present SML B library version;
2007-05-31, by wenzelm
tuned USEDIR_OPTIONS;
2007-05-30, by wenzelm
removed HOL4 image, which seldom works;
2007-05-30, by wenzelm
simplified data setup
2007-05-30, by haftmann
instance: always print sorts on failure
2007-05-30, by haftmann
more example
2007-05-30, by haftmann
fixed typo
2007-05-30, by haftmann
updated
2007-05-30, by haftmann
generalized lemmas
2007-05-30, by haftmann
eliminated strings
2007-05-30, by haftmann
tuned
2007-05-30, by haftmann
clarified error message
2007-05-30, by krauss
simplify names of locale interpretations
2007-05-30, by huffman
renamed some lemmas in Complex.thy
2007-05-30, by huffman
cleaned up proofs; reorganized sections; removed redundant lemmas
2007-05-30, by huffman
use new-style instance declarations
2007-05-29, by huffman
instance complex :: banach
2007-05-29, by huffman
add lemma real_sqrt_sum_squares_less
2007-05-29, by huffman
cleaned up some proofs
2007-05-29, by huffman
interpretation bounded_linear_divide
2007-05-29, by huffman
add bounded_linear lemmas
2007-05-29, by huffman
add isUCont lemmas
2007-05-29, by huffman
updated examples to include an instance of (lexicographic_order simp:...)
2007-05-29, by krauss
Complex: generalized type of exp
2007-05-28, by huffman
generalized exp to work over any complete field; new proof of exp_add
2007-05-28, by huffman
add type annotations for exp
2007-05-28, by huffman
interpretations additive_scaleR_left, additive_scaleR_right
2007-05-28, by huffman
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
2007-05-28, by huffman
new proof of Cauchy product formula for series
2007-05-27, by huffman
What it says
2007-05-26, by nipkow
improved error handling
2007-05-25, by haftmann
using rudimentary class target mechanism
2007-05-25, by haftmann
*** empty log message ***
2007-05-25, by haftmann
fixed typo
2007-05-25, by haftmann
fix typos
2007-05-25, by huffman
*** empty log message ***
2007-05-25, by nipkow
*** empty log message ***
2007-05-25, by nipkow
*** empty log message ***
2007-05-25, by nipkow
tuned
2007-05-25, by nipkow
Added List_Comprehension
2007-05-25, by nipkow
adapted to fix for fresh_fun_simp
2007-05-25, by urbanc
took out Class.thy from the compiling process until memory problems are solved
2007-05-25, by urbanc
simplify some proofs
2007-05-25, by huffman
*** empty log message ***
2007-05-24, by nipkow
Squared things out.
2007-05-24, by obua
fix a bug : the semantics of no_asm was the opposite
2007-05-24, by narboux
temporary fix for a bug in fresh_fun_simp
2007-05-24, by urbanc
formalisation of my PhD (the result was correct, but the proof needed several corrections)
2007-05-24, by urbanc
add an option in fresh_fun_simp to prevent rewriting in assumptions
2007-05-24, by narboux
fixes tvar issue in type inference
2007-05-24, by haftmann
tuned
2007-05-24, by haftmann
tuned warning
2007-05-24, by haftmann
rudimentary class target implementation
2007-05-24, by haftmann
tuned Pure/General/name_space.ML
2007-05-24, by haftmann
Introduced new classes monoid_add and group_add
2007-05-24, by nipkow
add lemma complete_algebra_summable_geometric
2007-05-23, by huffman
formatting
2007-05-23, by paulson
generalize powerseries and termdiffs lemmas using axclasses
2007-05-23, by huffman
remove unused simproc definition
2007-05-23, by huffman
remove redundant simproc; remove legacy ML bindings
2007-05-23, by huffman
remove redundant simproc
2007-05-23, by huffman
new simp rule Infinitesimal_of_hypreal_iff
2007-05-22, by huffman
removed redundant lemmas
2007-05-22, by huffman
generalize uniqueness of limits to class real_normed_algebra_1
2007-05-22, by huffman
Some hacks for SPASS format
2007-05-22, by paulson
some optimizations, cleanup
2007-05-22, by krauss
add missing instance declarations
2007-05-22, by huffman
adjusted to change in Provers/Arith/combine_numerals.ML
2007-05-22, by haftmann
adjusted to change in Provers/Arith/combine_numerals.ML
2007-05-22, by haftmann
regression tests: send failure reports to krauss@in.tum.de, too
2007-05-22, by krauss
rename lemmas LIM_ident, isCont_ident, DERIV_ident
2007-05-22, by huffman
remove obsolete CSeries.thy
2007-05-22, by huffman
generalized ring_eq_cancel simprocs to class idom; removed redundant field_eq_cancel simprocs
2007-05-22, by huffman
new field_combine_numerals simproc, which uses fractions as coefficients
2007-05-21, by huffman
search bottom up to get the inner fresh fun
2007-05-21, by narboux
add a bottom up search function
2007-05-21, by narboux
tuned
2007-05-21, by haftmann
evaluation for integers
2007-05-21, by haftmann
added lemma divAlg_div_mof
2007-05-21, by haftmann
improved code for rev
2007-05-21, by haftmann
min/max
2007-05-21, by haftmann
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
2007-05-21, by huffman
add lemmas divide_numeral_1 and inverse_numeral_1
2007-05-21, by huffman
fixed signature
2007-05-21, by krauss