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.
OuterKeyword;
2005-08-16, by wenzelm
updated;
2005-08-16, by wenzelm
removed -H false;
2005-08-16, by wenzelm
isatool usedir: option -V and -f;
2005-08-16, by wenzelm
tuned antiquotations;
2005-08-16, by wenzelm
\isabellestyleit: proper \isacharbackslash;
2005-08-16, by wenzelm
proper ML_DBASE for .../bin/poly;
2005-08-16, by wenzelm
added option -V VERSION;
2005-08-16, by wenzelm
added option -n NAME and -t TAGS;
2005-08-16, by wenzelm
-V outline=/proof,/ML;
2005-08-16, by wenzelm
* Command tags control specific markup of certain regions of text (replaces usedir -H);
2005-08-16, by wenzelm
simp_depth warning now mod 20, not mod 10 (too often)
2005-08-16, by nipkow
lucas - added pretty printing function and cleaned up signature a little.
2005-08-15, by dixon
lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing.
2005-08-15, by dixon
New command: interpretation in locales.
2005-08-10, by ballarin
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
2005-08-09, by nipkow
exported after_qed for arity proofs
2005-08-09, by haftmann
added finite(option) to Recdef.thy
2005-08-09, by nipkow
added selectors 'classes_of' and 'classes_arities_of'
2005-08-09, by haftmann
exported dest_def
2005-08-09, by haftmann
added 'the_const_constraint'
2005-08-09, by haftmann
(added to repository)
2005-08-09, by haftmann
(added to repository)
2005-08-09, by haftmann
After_qed takes result argument.
2005-08-08, by ballarin
Release of interpretation in locale.
2005-08-08, by ballarin
fixed typo in ratadd
2005-08-08, by nipkow
added hint for position of aqu options in connection with styles
2005-08-08, by haftmann
clarified ML_idf
2005-08-08, by haftmann
moved some rat functions to library.ML
2005-08-07, by nipkow
added more rat functions
2005-08-07, by nipkow
Tuned comment.
2005-08-06, by berghofe
new lemma
2005-08-06, by nipkow
Added ENTCS 2000 paper by Aleksey Nogin.
2005-08-05, by berghofe
New case study: pigeonhole principle.
2005-08-05, by berghofe
Added Extraction/Pigeonhole.
2005-08-05, by berghofe
added Brian Hufmann's finite instances
2005-08-05, by nipkow
Fixed bug in code generator for let and split leading to ill-formed code.
2005-08-03, by berghofe
Adapted to new argument format of MinProof constructor.
2005-08-03, by berghofe
Adapted to new interface og thms_of_proof / axms_of_proof.
2005-08-03, by berghofe
Adapted to new interface of thms_of_proof.
2005-08-03, by berghofe
- Tuned handling of oracles
2005-08-03, by berghofe
mentioned change to exp_ge_add_one_self, new transitivity rules
2005-08-03, by avigad
changes from renaming of exp_ge_add_one_self
2005-08-03, by avigad
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
2005-08-03, by avigad
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
2005-08-03, by avigad
added extra transitivity rules
2005-08-03, by avigad
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
2005-08-03, by avigad
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
2005-08-03, by avigad
import FixedPoint instead of Gfp
2005-08-03, by avigad
removed Gfp
2005-08-03, by avigad
removed Lfp
2005-08-03, by avigad
combined Lfp and Gfp to FixedPoint
2005-08-03, by avigad
tuned ML_OPTIONS;
2005-08-02, by wenzelm
export clear_ss;
2005-08-02, by wenzelm
added unfold_tac (Simplifier.inherit_bounds);
2005-08-02, by wenzelm
simprocs: Simplifier.inherit_bounds;
2005-08-02, by wenzelm
tuned;
2005-08-02, by wenzelm
First version of interpretation in locales. Not yet fully functional.
2005-08-02, by ballarin
Turned simp_implies into binary operator.
2005-08-02, by ballarin
Added filter lemma
2005-08-02, by nipkow
* Pure/Simplifier: improved handling of bound variables;
2005-08-01, by wenzelm
determine Poly/ML runtime system version
2005-08-01, by wenzelm
obsolete;
2005-08-01, by wenzelm
determine Poly/ML's idea of current hardware and operating system type;
2005-08-01, by wenzelm
tuned;
2005-08-01, by wenzelm
Thm.full_prop_of;
2005-08-01, by wenzelm
Compress.term;
2005-08-01, by wenzelm
removed atless (use term_ord instead);
2005-08-01, by wenzelm
export MataSimplifier.inherit_bounds;
2005-08-01, by wenzelm
Compress.typ;
2005-08-01, by wenzelm
Compress.init_data;
2005-08-01, by wenzelm
nameless Term.bound;
2005-08-01, by wenzelm
improved bounds: nameless Term.bound, recover names for output;
2005-08-01, by wenzelm
tuned dict_ord;
2005-08-01, by wenzelm
replaced atless by term_ord;
2005-08-01, by wenzelm
chain_history: turned into runtime flag;
2005-08-01, by wenzelm
compression of terms and types by sharing common subtrees;
2005-08-01, by wenzelm
added compress.ML;
2005-08-01, by wenzelm
Term.is_bound;
2005-08-01, by wenzelm
tuned signature;
2005-08-01, by wenzelm
no eq_commute;
2005-08-01, by wenzelm
Defs.monomorphic;
2005-08-01, by wenzelm
Sign.read_term;
2005-08-01, by wenzelm
more zcong_sym;
2005-08-01, by wenzelm
simprocs: Simplifier.inherit_bounds;
2005-08-01, by wenzelm
no eq_sym_conv;
2005-08-01, by wenzelm
removed read_cterm;
2005-08-01, by wenzelm
tuned msg;
2005-08-01, by wenzelm
PolyML.Compiler.printInAlphabeticalOrder := false;
2005-08-01, by wenzelm
polyml: use polyml-platform/version from Isabelle distribution;
2005-08-01, by wenzelm
obsolete;
2005-08-01, by wenzelm
1. changed configuration variables for linear programming (Cplex_tools):
2005-08-01, by obua
added map_filter lemmas
2005-08-01, by nipkow
Ordering is now: first by number of assumptions, second by the substitution size.
2005-08-01, by kleing
addedd ID line
2005-07-30, by nipkow
mentioned Ln in NEWS
2005-07-29, by avigad
fixed minor typo in comments
2005-07-29, by avigad
changed import to Ln
2005-07-29, by avigad
added a new theory; properties of ln
2005-07-29, by avigad
P.opt_locale_target;
2005-07-29, by wenzelm
nameless theorems: better names, flag to omit them
2005-07-29, by paulson
invents theorem names; also patches write_out_clasimp
2005-07-28, by paulson
dead code
2005-07-28, by paulson
new function trim_ends
2005-07-28, by paulson
uniform treatment of variable prefixes
2005-07-28, by paulson
corrected some typos
2005-07-28, by haftmann
new droplet
2005-07-28, by paulson
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
2005-07-28, by quigley
tuned gen_all, forall_elim_list, implies_intr_list, standard;
2005-07-28, by wenzelm
Sign.typ_unify;
2005-07-28, by wenzelm
Sign.typ_unify;
2005-07-28, by wenzelm
typ_match, unify: canonical argument order;
2005-07-28, by wenzelm
added weaken, adjust_maxidx_thm;
2005-07-28, by wenzelm
check_overloading replaces datatype overloading;
2005-07-28, by wenzelm
added add_tfreesT, add_tfrees;
2005-07-28, by wenzelm
norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
2005-07-28, by wenzelm
added add_const_constraint(_i), const_constraint;
2005-07-28, by wenzelm
adapted Type.typ_match;
2005-07-28, by wenzelm
Sign.typ_unify;
2005-07-28, by wenzelm
Term.bound;
2005-07-28, by wenzelm
print_theory: const constraints;
2005-07-28, by wenzelm
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
2005-07-28, by wenzelm
Sign.typ_match;
2005-07-28, by wenzelm
Sign.typ_unify;
2005-07-28, by wenzelm
fixed var index in tactic;
2005-07-28, by wenzelm
proper header;
2005-07-28, by wenzelm
Sign.typ_instance;
2005-07-28, by wenzelm
updated;
2005-07-28, by wenzelm
tuned;
2005-07-28, by wenzelm
now for Mailman-enabled mailing list
2005-07-28, by paulson
now for Mailman-enabled mailing list
2005-07-28, by paulson
now for Mailman-enabled mailing list
2005-07-28, by paulson
simpler variable names, and no types for monomorphic constants
2005-07-27, by paulson
removed the dependence on abs_mult
2005-07-27, by paulson
fixed typo
2005-07-26, by huffman
brought ML files up to date with new lemmas
2005-07-26, by huffman
renamed Exh_Ssum1 to Exh_Ssum; cleaned up
2005-07-26, by huffman
cleaned up
2005-07-26, by huffman
removed duplicated code; generate new lub and thelub lemmas for new cpo types
2005-07-26, by huffman
cleaned up; renamed some theorems
2005-07-26, by huffman
add theorem fix_defined_iff; cleaned up
2005-07-26, by huffman
add theorem cpair_defined_iff
2005-07-26, by huffman
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
2005-07-26, by webertj
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
2005-07-26, by webertj
comment modified
2005-07-26, by webertj
write_dimacs_sat_file writes outer parentheses again
2005-07-26, by webertj
replaced calls to PropLogic.defcnf by PropLogic.auxcnf
2005-07-26, by webertj
minor parameter changes
2005-07-26, by webertj
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
2005-07-25, by webertj
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
2005-07-25, by avigad
defcnf modified to internally use a reference
2005-07-25, by webertj
dead code removal
2005-07-22, by paulson
reformatting and tidying
2005-07-22, by paulson
tidied up the tracing output
2005-07-22, by paulson
streamlined the tptp output
2005-07-22, by paulson
removed unused code
2005-07-22, by paulson
Tuned comment.
2005-07-22, by berghofe
Rewrote function remove_suc, since it failed on some equations
2005-07-22, by berghofe
write_dimacs_sat_file now generates slightly smaller files
2005-07-21, by webertj
revised examples
2005-07-20, by paulson
code streamlining
2005-07-20, by paulson
Ressurect seq attribute accidently removed
2005-07-20, by aspinall
Sort search results in order of relevance, where relevance =
2005-07-20, by kleing
Inttab.defined;
2005-07-19, by wenzelm
some structured proofs on completeness;
2005-07-19, by wenzelm
more contribs;
2005-07-19, by wenzelm
tuned;
2005-07-19, by wenzelm
isatool fixheaders;
2005-07-19, by wenzelm
with_path;
2005-07-19, by wenzelm
added list of theorem changes to NEWS
2005-07-19, by avigad
added defined;
2005-07-19, by wenzelm
simplified union;
2005-07-19, by wenzelm
tuned match, unify;
2005-07-19, by wenzelm
tuned instantiate (avoid subst_atomic, subst_atomic_types);
2005-07-19, by wenzelm
tuned defs interface;
2005-07-19, by wenzelm
moved incr_tvar to logic.ML;
2005-07-19, by wenzelm
tuned norm_sort, mg_domain;
2005-07-19, by wenzelm
tuned instantiate interface;
2005-07-19, by wenzelm
incr_tvar (from term.ML), incr_indexes: avoid garbage;
2005-07-19, by wenzelm
added has_duplicates;
2005-07-19, by wenzelm
tuned interfaces declare, define, finalize, merge:
2005-07-19, by wenzelm
Logic.incr_tvar;
2005-07-19, by wenzelm
retract accidental user commit;
2005-07-19, by wenzelm
tuned;
2005-07-19, by wenzelm
proving bounds for real linear programs
2005-07-19, by obua
removed some garbage;
2005-07-19, by schirmer
textual tweak
2005-07-19, by paulson
Documentation updated
2005-07-18, by webertj
reverted from fold_yield to fold_map
2005-07-18, by haftmann
*** empty log message ***
2005-07-15, by wenzelm
tuned fold on terms and lists;
2005-07-15, by wenzelm
tuned assoc;
2005-07-15, by wenzelm
tuned fold on terms;
2005-07-15, by wenzelm
tuned min_key, max_key;
2005-07-15, by wenzelm
replaced foldl_XXX by canonical fold_XXX;
2005-07-15, by wenzelm
tuned;
2005-07-15, by wenzelm
tuned fold on terms;
2005-07-15, by wenzelm
* Pure/library.ML: several combinators for linear functional transformations;
2005-07-15, by wenzelm
optimize no_types_needed, remove exception handler
2005-07-15, by obua
tuned;
2005-07-15, by wenzelm
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
2005-07-14, by dixon
* Improved 'oracle' command -- type-safe;
2005-07-14, by wenzelm
no open Logic;
2005-07-14, by wenzelm
removed itlist, rev_itlist -- use fold_rev, fold instead;
2005-07-14, by wenzelm
replaced itlist by fold_rev;
2005-07-14, by wenzelm
replaced itlist by fold_rev;
2005-07-14, by wenzelm
use sys_error instead of exception Internal;
2005-07-14, by wenzelm
sys_error;
2005-07-14, by wenzelm
type-safe 'oracle' command;
2005-07-14, by wenzelm
added dest_table;
2005-07-14, by wenzelm
invoke_oracle: do not keep theory value, but theory_ref;
2005-07-14, by wenzelm
occs no longer infix (structure not open);
2005-07-14, by wenzelm
NameSpace.dest_table avoids duplicated extern;
2005-07-14, by wenzelm
with_path;
2005-07-14, by wenzelm
removed mk_prodT, mk_not (cf. HOL/hologic.ML);
2005-07-14, by wenzelm
tuned;
2005-07-14, by wenzelm
use all files in HOLCF.thy;
2005-07-14, by wenzelm
replaced Utils.itlist by fold_rev;
2005-07-14, by wenzelm
proper structure;
2005-07-14, by wenzelm
use existing Inttab;
2005-07-14, by wenzelm
improved oracle setup;
2005-07-14, by wenzelm
improved oracle setup;
2005-07-14, by wenzelm
removed not_const -- use Not instead;
2005-07-14, by wenzelm
HOL.Not;
2005-07-14, by wenzelm
HOL.Not;
2005-07-14, by wenzelm
new type-safe interface;
2005-07-14, by wenzelm
removed FOL/ex/IffOracle.ML;
2005-07-14, by wenzelm
obsolete;
2005-07-14, by wenzelm
improved 'oracle' command;
2005-07-14, by wenzelm
tuned;
2005-07-14, by wenzelm
accomodate change of real_of_XXX;
2005-07-14, by wenzelm
- fixed bug concerning the renaming of axiom names
2005-07-14, by obua
added ` combinator
2005-07-14, by haftmann
(fix for smlnj)
2005-07-14, by haftmann
simplified proof of cont_Iwhen3
2005-07-14, by huffman
avoiding even more garbage
2005-07-13, by schirmer
Update PGIP packet handling, fixing unique session identifier.
2005-07-13, by aspinall
fixed typos in theorem names
2005-07-13, by avigad
Additions to the Real (and Hyperreal) libraries:
2005-07-13, by avigad
tidied
2005-07-13, by paulson
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip