Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
moved the_single to Pure/library.ML;
2006-10-07, by wenzelm
TheoryTarget.init;
2006-10-07, by wenzelm
tuned comments;
2006-10-07, by wenzelm
tuned method syntax: polymorhic term argument;
2006-10-07, by wenzelm
tuned;
2006-10-07, by wenzelm
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
2006-10-06, by paulson
Tidied code to delete tmp files.
2006-10-06, by paulson
renamed the combinator laws
2006-10-06, by paulson
Improved detection of identical clauses, also in the conjecture
2006-10-06, by paulson
Refinements to abstraction. Seeding with combinators K, I and B.
2006-10-06, by paulson
examples for hex and bin numerals
2006-10-06, by kleing
Changed and removed some functions related to combinators, since they are Isabelle constants now.
2006-10-05, by mengj
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
2006-10-05, by paulson
improvements to abstraction, ensuring more re-use of abstraction functions
2006-10-05, by paulson
facts about combinators
2006-10-05, by paulson
a few new functions on thms and cterms
2006-10-05, by paulson
reorganize and speed up termdiffs proofs
2006-10-05, by huffman
fixed bug in linear arith
2006-10-04, by nipkow
improvements for Haskell serialization
2006-10-04, by haftmann
insert replacing ins ins_int ins_string
2006-10-04, by haftmann
cleaned up some mess
2006-10-04, by haftmann
clarified header comments
2006-10-04, by haftmann
insert replacing ins ins_int ins_string
2006-10-04, by haftmann
*** empty log message ***
2006-10-04, by haftmann
tuned
2006-10-04, by webertj
Improved error reporting
2006-10-04, by krauss
nnf_simpset built statically
2006-10-04, by webertj
rewrite proofs of powser_insidea and termdiffs_aux
2006-10-03, by huffman
generalize summability lemmas using class banach
2006-10-02, by huffman
clarified setup name
2006-10-02, by haftmann
various code refinements
2006-10-02, by haftmann
fixed some Haskell issues
2006-10-02, by haftmann
changed preprocessing framework
2006-10-02, by haftmann
clarified some things
2006-10-02, by haftmann
cleaned and extended
2006-10-02, by haftmann
added gen_primrec
2006-10-02, by haftmann
added code for insert
2006-10-02, by haftmann
improvements for code_gen
2006-10-02, by haftmann
cleaned mess
2006-10-02, by haftmann
added example for code_gen
2006-10-02, by haftmann
dropped obsolete Theory.sign_of
2006-10-02, by haftmann
tuned
2006-10-02, by haftmann
added code generator names for nat_rec and nat_case
2006-10-02, by haftmann
improved serialization for arbitrary
2006-10-02, by haftmann
normal_form now a diagnostic command
2006-10-02, by haftmann
restructured contents
2006-10-02, by haftmann
add axclass banach for complete normed vector spaces
2006-10-02, by huffman
remove unused Cauchy_Bseq lemmas
2006-10-02, by huffman
add lemmas norm_not_less_zero, norm_le_zero_iff
2006-10-02, by huffman
added is_Trueprop
2006-10-02, by paulson
tidying and simplifying
2006-10-02, by paulson
Changing the default for theory_const
2006-10-02, by paulson
extensions for Susanto
2006-10-02, by paulson
restored the "length of name > 2" check for package definitions
2006-10-02, by paulson
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
2006-10-02, by paulson
exists_name: include this theory name;
2006-10-01, by wenzelm
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-10-01, by wenzelm
merged with theory Datatype_Universe;
2006-10-01, by wenzelm
obsolete;
2006-10-01, by wenzelm
renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
2006-10-01, by wenzelm
removed share_data;
2006-10-01, by wenzelm
cterm_match: avoid recalculation of maxidx;
2006-10-01, by wenzelm
reverted to revision 1.28;
2006-10-01, by wenzelm
proper use of svc_oracle.ML;
2006-10-01, by wenzelm
reactivated theory PER;
2006-10-01, by wenzelm
tuned proofs;
2006-10-01, by wenzelm
moved theory Infinite_Set to Library;
2006-10-01, by wenzelm
moved theory Infinite_Set to Library;
2006-10-01, by wenzelm
moved Infinite_Set.thy to Library;
2006-10-01, by wenzelm
tuned;
2006-10-01, by wenzelm
Removed the helper files (combinator rewrite rules, function extensionality and fequal rules).
2006-10-01, by mengj
generalize more DERIV proofs
2006-10-01, by huffman
statement: Variable.fix_frees;
2006-09-30, by wenzelm
added undo_end;
2006-09-30, by wenzelm
tuned proofs;
2006-09-30, by wenzelm
proper import of Main HOL;
2006-09-30, by wenzelm
tuned specifications and proofs;
2006-09-30, by wenzelm
hides popular names (from Datatype.thy);
2006-09-30, by wenzelm
removed obsolete sum_case_Inl/Inr;
2006-09-30, by wenzelm
renamed Variable.invent_fixes to Variable.variant_fixes;
2006-09-30, by wenzelm
generalize proofs of DERIV_isCont and DERIV_mult
2006-09-30, by huffman
generalized some DERIV proofs
2006-09-30, by huffman
add scaleR lemmas
2006-09-30, by huffman
generalize type of DERIV
2006-09-30, by huffman
add type annotations for DERIV
2006-09-30, by huffman
Combinator axioms are now from Isabelle theorems, no need to use helper files.
2006-09-30, by mengj
Added the combinator constants to the constants table.
2006-09-30, by mengj
Removed ResHolClause.LAM2COMB exception.
2006-09-30, by mengj
Reordered how files are loaded.
2006-09-30, by mengj
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
2006-09-29, by wenzelm
removed mixfix_content;
2006-09-29, by wenzelm
Syntax.mode;
2006-09-29, by wenzelm
Syntax.mode;
2006-09-29, by wenzelm
Sign.add_consts_authentic;
2006-09-29, by wenzelm
proper use of matrixlp.ML;
2006-09-29, by wenzelm
simplified is_package_def -- be less ambitious about B library operations;
2006-09-29, by wenzelm
obsolete;
2006-09-28, by wenzelm
added share_data;
2006-09-28, by wenzelm
Sign.add_consts_authentic;
2006-09-28, by wenzelm
consts: syntax consts only for actual syntax;
2006-09-28, by wenzelm
added share_data (dummy);
2006-09-28, by wenzelm
removed obsolete HOLCF.ML;
2006-09-28, by wenzelm
ResAtpset.get_atpset;
2006-09-28, by wenzelm
removed legacy code;
2006-09-28, by wenzelm
tuned definitions/proofs;
2006-09-28, by wenzelm
proper use of float.ML;
2006-09-28, by wenzelm
fixed translations: CONST;
2006-09-28, by wenzelm
replaced syntax/translations by abbreviation;
2006-09-28, by wenzelm
replaced syntax/translations by abbreviation;
2006-09-28, by wenzelm
removed obsolete Real/document/root.tex;
2006-09-28, by wenzelm
tuned;
2006-09-28, by wenzelm
rearranged axioms and simp rules for scaleR
2006-09-28, by huffman
added Poly/ML 4.9.1 (experimental!);
2006-09-28, by wenzelm
rearranged axioms and simp rules for scaleR
2006-09-28, by huffman
clearout of obsolete code
2006-09-28, by paulson
addition of combinators
2006-09-28, by paulson
tuned messages;
2006-09-28, by wenzelm
tuned;
2006-09-28, by wenzelm
LD_LIBRARY_PATH;
2006-09-28, by wenzelm
Definitions produced by packages are now blacklisted.
2006-09-28, by paulson
more reorganizing sections
2006-09-28, by huffman
reorganize sections
2006-09-28, by huffman
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
2006-09-28, by huffman
add lemma hypreal_epsilon_gt_zero
2006-09-28, by huffman
generalize type of is(NS)UCont
2006-09-28, by huffman
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
2006-09-28, by huffman
proper use of PolyML.shareCommonData;
2006-09-28, by wenzelm
add lemmas InfinitesimalI2, InfinitesimalD2
2006-09-27, by huffman
adapted to pre-5.0 versions;
2006-09-27, by wenzelm
Poly/ML startup script (for 4.9.1);
2006-09-27, by wenzelm
added ML-Systems/polyml-4.9.1.ML;
2006-09-27, by wenzelm
Compatibility wrapper for Poly/ML 4.9.1.
2006-09-27, by wenzelm
removed all references to star_n and FreeUltrafilterNat
2006-09-27, by huffman
add lemmas about hnorm, Infinitesimal
2006-09-27, by huffman
reverted to 1.58;
2006-09-27, by wenzelm
proper const_syntax for uminus, abs;
2006-09-27, by wenzelm
reorganized HNatInfinite proofs; simplified and renamed some lemmas
2006-09-27, by huffman
removed obsolete of_instream_slurp -- now already included in tty;
2006-09-27, by wenzelm
Source.tty now slurps by default;
2006-09-27, by wenzelm
of_stream/tty: slurp input eagerly;
2006-09-27, by wenzelm
tuned all_paths;
2006-09-27, by wenzelm
internal params: Vartab instead of AList;
2006-09-27, by wenzelm
removed unused serial_of, name_of;
2006-09-27, by wenzelm
removed redundant lemmas;
2006-09-27, by wenzelm
remove redundant lemmas
2006-09-27, by huffman
replaced constant 0 by HOL.zero
2006-09-27, by haftmann
hypreal_of_nat abbreviates of_nat
2006-09-27, by huffman
add lemmas of_real_eq_star_of, Reals_eq_Standard
2006-09-27, by huffman
move star_of_norm from SEQ.thy to NSA.thy
2006-09-27, by huffman
convert more proofs to transfer principle
2006-09-27, by huffman
add lemmas about Standard, real_of, scaleR
2006-09-27, by huffman
instance complex :: real_normed_field; cleaned up
2006-09-27, by huffman
add lemma stc_unique; shorten stc proofs
2006-09-27, by huffman
add lemmas approx_diff and st_unique, shorten st proofs
2006-09-27, by huffman
add lemmas about of_real and power
2006-09-27, by huffman
reorganize section headings
2006-09-27, by huffman
more lemmas about Standard and star_of
2006-09-27, by huffman
define new constant Standard = range star_of
2006-09-27, by huffman
add lemmas of_int_in_Reals, of_nat_in_Reals
2006-09-27, by huffman
add header
2006-09-26, by huffman
Changed precedence of "op O" (relation composition) from 60 to 75.
2006-09-26, by krauss
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
2006-09-26, by haftmann
tuned syntax for <= <
2006-09-26, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-26, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly
2006-09-26, by haftmann
fixed the definition of "depth"
2006-09-26, by paulson
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
2006-09-26, by paulson
some cleanup
2006-09-25, by haftmann
changed order
2006-09-25, by haftmann
inserted headings
2006-09-25, by haftmann
changed interface in codegen_package.ML
2006-09-25, by haftmann
fixed some mess
2006-09-25, by haftmann
cleaned up
2006-09-25, by haftmann
adding constants the modern way
2006-09-25, by haftmann
added examples for variable name handling
2006-09-25, by haftmann
better handling for div by zero
2006-09-25, by haftmann
updated theory description
2006-09-25, by haftmann
refinements in codegen serializer
2006-09-25, by haftmann
added 'undefined' serializer
2006-09-25, by haftmann
added code_instname
2006-09-25, by haftmann
reorganized subsection headings
2006-09-24, by huffman
moved SEQ_Infinitesimal from SEQ to HyperNat
2006-09-24, by huffman
real_norm_def [simp]
2006-09-24, by huffman
generalize types of lim and nslim
2006-09-24, by huffman
generalized types of sums, summable, and suminf
2006-09-24, by huffman
add lemma convergent_Cauchy
2006-09-24, by huffman
remove extra dependencies
2006-09-24, by huffman
add proof of summable_LIMSEQ_zero
2006-09-24, by huffman
change definitions from SOME to THE
2006-09-24, by huffman
move root and sqrt stuff from Transcendental to NthRoot
2006-09-24, by huffman
fix proof
2006-09-24, by huffman
added lemmas about LIMSEQ and norm; simplified some proofs
2006-09-22, by huffman
add lemma norm_power
2006-09-22, by huffman
added HOL-Complex-ex;
2006-09-22, by wenzelm
define constants with THE instead of SOME
2006-09-22, by huffman
Fixed bug concerning the generation of identifiers for
2006-09-22, by berghofe
Replaced irreducible_paths by all_paths.
2006-09-22, by berghofe
Added function all_paths (formerly find_paths).
2006-09-22, by berghofe
tuned proofs;
2006-09-22, by wenzelm
tuned oracle name;
2006-09-21, by wenzelm
added is_ml_reserved;
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
serial numbers for types;
2006-09-21, by wenzelm
added dest_binop;
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
tuned eta_contract;
2006-09-21, by wenzelm
added dest_equals_rhs;
2006-09-21, by wenzelm
tuned;
2006-09-21, by wenzelm
serial numbers for consts;
2006-09-21, by wenzelm
Thm.dest_binop;
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
member (op =);
2006-09-21, by wenzelm
updated timings;
2006-09-21, by wenzelm
new function hashw_int
2006-09-21, by paulson
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
2006-09-21, by paulson
corrected for the translation from _ to __ in c_COMBx_e
2006-09-21, by paulson
changed constants into abbreviations; shortened proofs
2006-09-21, by huffman
XML syntax for types, terms, and proofs.
2006-09-21, by berghofe
Added xml_syntax.ML
2006-09-21, by berghofe
Added Tools/xml_syntax.ML
2006-09-21, by berghofe
circumvented defect in SML/NJ type inference
2006-09-21, by haftmann
1. Function package accepts a parameter (default "some_term"), which specifies the functions
2006-09-21, by krauss
removed division_by_zero class requirements from several lemmas
2006-09-21, by huffman
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
2006-09-21, by huffman
choose gnuplot terminal by platform
2006-09-20, by isatest
set terminal png color -- works for older versions of gnuplot;
2006-09-20, by wenzelm
added ZF-UNITY;
2006-09-20, by wenzelm
tidied
2006-09-20, by paulson
Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
2006-09-20, by mengj
make it work on sunbroy2
2006-09-20, by isatest
Moved the functional equality axioms to helper1 files.
2006-09-20, by mengj
Introduced combinators B', C' and S'.
2006-09-20, by mengj
Removed include_min_comb and include_combS.
2006-09-20, by mengj
Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
2006-09-20, by aspinall
improvements for codegen 2
2006-09-20, by haftmann
name shifts
2006-09-20, by haftmann
fixed bug
2006-09-20, by haftmann
Removed "induct set" attribute from total induction rules
2006-09-20, by krauss
removed debug
2006-09-20, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip