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.
renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;
2009-01-02, by wenzelm
removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;
2009-01-02, by wenzelm
updated rendering of inner token markup;
2009-01-02, by wenzelm
more detailed inner token markup;
2009-01-02, by wenzelm
added numeral, which supercedes num, xnum, float;
2009-01-02, by wenzelm
renamed token markup "_xstr" to "_inner_string";
2009-01-02, by wenzelm
removed dead code;
2009-01-02, by wenzelm
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
2009-01-02, by wenzelm
tuned;
2009-01-02, by wenzelm
Isar.command: plain Position.id;
2009-01-02, by wenzelm
added type 'a parser, simplified signature;
2009-01-02, by wenzelm
added type 'a parser, simplified signature;
2009-01-02, by wenzelm
added type 'a parser, simplified signature;
2009-01-02, by wenzelm
added props_text (from outer_parse.ML);
2009-01-02, by wenzelm
added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
2009-01-02, by wenzelm
added id;
2009-01-02, by wenzelm
MetaSimplifier.SIMPLIFIER;
2009-01-02, by wenzelm
fixed assumption proof;
2009-01-02, by wenzelm
tuned header and description of boot files;
2009-01-02, by wenzelm
merged;
2009-01-01, by wenzelm
normalized some ML type/val aliases;
2009-01-01, by wenzelm
assumption/close: discontinued implicit prems;
2009-01-01, by wenzelm
avoid implicit use of prems;
2009-01-01, by wenzelm
updated generated files;
2009-01-01, by wenzelm
eliminated implicit use of prems;
2009-01-01, by wenzelm
updated generated files;
2009-01-01, by wenzelm
updated type 'a lazy;
2009-01-01, by wenzelm
proper import of ~~/src/HOL/ex/ReflectedFerrack;
2009-01-01, by wenzelm
crude adaption to intermediate class/locale version;
2009-01-01, by wenzelm
crude adaption to new locales;
2009-01-01, by wenzelm
avoid implicit prems -- tuned proofs;
2009-01-01, by wenzelm
avoid implicit use of prems;
2009-01-01, by wenzelm
Term.add_consts;
2009-01-01, by wenzelm
eliminated OldTerm.(add_)term_consts;
2009-01-01, by wenzelm
avoid polymorphic equality;
2009-01-01, by wenzelm
eliminated OldTerm.(add_)term_consts;
2009-01-01, by wenzelm
added canonical add_const_names, add_consts;
2009-01-01, by wenzelm
provide structure CharVector;
2009-01-01, by wenzelm
isabelle-process;
2009-01-01, by wenzelm
updated sessions;
2009-01-01, by wenzelm
removed unused add_term_free_names;
2008-12-31, by wenzelm
eliminated OldTerm.add_term_free_names;
2008-12-31, by wenzelm
updated header;
2008-12-31, by wenzelm
Term.declare_typ_names, Term.declare_term_frees;
2008-12-31, by wenzelm
added declare_term_frees;
2008-12-31, by wenzelm
Term.declare_term_frees;
2008-12-31, by wenzelm
qualified Term.rename_wrt_term;
2008-12-31, by wenzelm
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31, by wenzelm
use fold_aterms directly;
2008-12-31, by wenzelm
use exists_Const directly;
2008-12-31, by wenzelm
use regular Term.add_XXX etc.;
2008-12-31, by wenzelm
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31, by wenzelm
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31, by wenzelm
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-12-31, by wenzelm
use exists_subterm directly;
2008-12-31, by wenzelm
use exists_subterm directly;
2008-12-31, by wenzelm
use regular Term.add_vars, Term.add_frees etc.;
2008-12-31, by wenzelm
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-31, by wenzelm
use regular Term.add_vars, Term.add_frees etc.;
2008-12-31, by wenzelm
added old_term.ML;
2008-12-31, by wenzelm
Some old-style term operations.
2008-12-31, by wenzelm
freeze_thaw: canonical Term.add_XXX operations;
2008-12-30, by wenzelm
varify: regular name context;
2008-12-30, by wenzelm
canonical Term.add_var_names, Term.add_tvar_namesT;
2008-12-30, by wenzelm
canonical Term.add_var_names;
2008-12-30, by wenzelm
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
2008-12-30, by wenzelm
removed unused head_name_of;
2008-12-30, by wenzelm
merged
2008-12-30, by wenzelm
prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;
2008-12-30, by wenzelm
New locales.
2008-12-30, by ballarin
Merged.
2008-12-30, by ballarin
Temporarily avoid type errors in parse phase.
2008-12-30, by ballarin
More liberal consistency check for defines elements.
2008-12-23, by ballarin
All logics ported to new locales.
2008-12-19, by ballarin
Merged.
2008-12-19, by ballarin
adapted statespace module to new locales;
2008-12-18, by Norbert Schirmer
More porting to new locales.
2008-12-19, by ballarin
Intro_locales_tac knows about defines elements; more robust export morphism.
2008-12-19, by ballarin
More porting to new locales.
2008-12-19, by ballarin
Merged.
2008-12-19, by ballarin
More porting to new locales
2008-12-19, by ballarin
Merged.
2008-12-18, by ballarin
More porting to new locales.
2008-12-17, by ballarin
Prevent defines from being checked in interpretation.
2008-12-17, by ballarin
Merged.
2008-12-16, by ballarin
More porting to new locales.
2008-12-16, by ballarin
Merged.
2008-12-16, by ballarin
More porting to new locales.
2008-12-16, by ballarin
More porting to new locales.
2008-12-15, by ballarin
Ported HOL and HOL-Library to new locales.
2008-12-14, by ballarin
Fixed legacy locale keywords (went to ZF rather than default keywords file).
2008-12-14, by ballarin
Merged.
2008-12-14, by ballarin
Merged.
2008-12-12, by ballarin
Porting to new locales.
2008-12-12, by ballarin
Theory target distinguishes old and new locales.
2008-12-12, by ballarin
Merged.
2008-12-12, by ballarin
Ported to new locales.
2008-12-12, by ballarin
Merged; updated interpretation command in isar_syn.ML.
2008-12-12, by ballarin
Merged.
2008-12-11, by ballarin
Conversion of HOL-Main and ZF to new locales.
2008-12-11, by ballarin
Add inherited registrations.
2008-12-19, by ballarin
Refactored: evaluate specification text only in locale declarations.
2008-12-18, by ballarin
Transfer theorems in print_locale.
2008-12-17, by ballarin
Attributes not applied in foundational version of fact.
2008-12-17, by ballarin
Transfer morphism with theory closure.
2008-12-16, by ballarin
Finer-grained activation so that facts from earlier elements are available.
2008-12-16, by ballarin
Transfer theorems before activation.
2008-12-16, by ballarin
Use correct mode when parsing elements and conclusion.
2008-12-16, by ballarin
Strict prefixes in locales expressions.
2008-12-14, by ballarin
Propagate theorems to registrations.
2008-12-12, by ballarin
Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-12, by ballarin
Equations in interpretation as goals.
2008-12-12, by ballarin
Interpretation in theories: first version with equations.
2008-12-11, by ballarin
Clarified comment.
2008-12-11, by ballarin
Use prefix component of bindings for locale prefixes.
2008-12-10, by ballarin
Missing dependency
2008-12-10, by ballarin
Preserve idents (expression in sublocale).
2008-12-10, by ballarin
added POSITION_PROPERTIES;
2008-12-29, by wenzelm
tuned;
2008-12-29, by wenzelm
override toString method;
2008-12-29, by wenzelm
Swing utilities.
2008-12-29, by wenzelm
merged
2008-12-29, by wenzelm
optional exception logging;
2008-12-29, by wenzelm
merged
2008-12-29, by haftmann
pretty printer for bindings
2008-12-29, by haftmann
adapted HOL source structure to distribution layout
2008-12-29, by haftmann
tuned;
2008-12-29, by wenzelm
more markup elements;
2008-12-29, by wenzelm
tuned;
2008-12-29, by wenzelm
merged
2008-12-29, by wenzelm
explicit EventBus for results;
2008-12-29, by wenzelm
added methods "+" and "-";
2008-12-29, by wenzelm
Generic event bus.
2008-12-29, by wenzelm
eliminated fun/val confusion
2008-12-29, by haftmann
merged
2008-12-28, by huffman
clean up proofs of lemma Maclaurin
2008-12-28, by huffman
disabled old jedit plugin;
2008-12-28, by wenzelm
more markup elements;
2008-12-28, by wenzelm
more markup elements;
2008-12-28, by wenzelm
removed duplicate sum_case used only by function package;
2008-12-27, by krauss
tuned NEWS; CONTRIBUTORS
2008-12-27, by krauss
renamed LexOrds.thy to Termination.thy; examples for sizechange method
2008-12-27, by krauss
tuned;
2008-12-27, by wenzelm
merged
2008-12-27, by wenzelm
refined execute, which replaces exec/exec2;
2008-12-27, by wenzelm
maintain initial process environment;
2008-12-27, by wenzelm
merged
2008-12-27, by haftmann
tackling simultaneous val/fun bindings
2008-12-27, by haftmann
proper class IsabelleSystem -- no longer static;
2008-12-27, by wenzelm
PATH: /opt/local/bin is back again (required for latex etc.);
2008-12-27, by wenzelm
merged.
2008-12-24, by huffman
clean up lemmas about ln
2008-12-24, by huffman
clean up lemmas about exp
2008-12-24, by huffman
more proofs about differentiable
2008-12-24, by huffman
use less_iff_Suc_add instead of less_add_one
2008-12-24, by huffman
rearranged subsections; cleaned up some proofs
2008-12-24, by huffman
move theorems about limits from Transcendental.thy to Deriv.thy
2008-12-24, by huffman
cleaned up some proofs; removed redundant simp rules
2008-12-24, by huffman
move sin and cos to their own subsection
2008-12-23, by huffman
clean up some proofs; remove unused lemmas
2008-12-23, by huffman
tuned;
2008-12-23, by wenzelm
* Proofs of are run in parallel on multi-core systems;
2008-12-23, by wenzelm
updated generated file;
2008-12-23, by wenzelm
updated thread-safe programming;
2008-12-23, by wenzelm
updated generated file;
2008-12-23, by wenzelm
added float_token, and num_const, float_const;
2008-12-23, by wenzelm
renamed terminal category "float" to "float_token", to avoid name
2008-12-23, by wenzelm
manual file type setup using AppHack 1.1;
2008-12-23, by wenzelm
target PWD;
2008-12-23, by wenzelm
updated scala path;
2008-12-23, by wenzelm
added platform_file;
2008-12-23, by wenzelm
proper -X option;
2008-12-22, by wenzelm
unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
2008-12-22, by wenzelm
more sophisticated MacOS interface script (mostly for Carbon Emacs);
2008-12-22, by wenzelm
updated web style for Mercurial 1.1.1;
2008-12-21, by wenzelm
misc webstyle adaptions;
2008-12-21, by wenzelm
updated web style for Mercurial 1.1;
2008-12-20, by wenzelm
removed Ids;
2008-12-20, by wenzelm
merged
2008-12-20, by wenzelm
removed Ids;
2008-12-20, by wenzelm
merged.
2008-12-19, by huffman
constdefs -> definition
2008-12-18, by huffman
removed Ids;
2008-12-19, by wenzelm
merged.
2008-12-18, by huffman
remove cvs Id tags
2008-12-16, by huffman
merged
2008-12-17, by wenzelm
basic setup for MacOS application bundle;
2008-12-17, by wenzelm
GHC ext pragma in generated Haskell modules
2008-12-17, by haftmann
dropped Ids
2008-12-17, by haftmann
temporary adaption to new locale code
2008-12-17, by haftmann
restructured; circumvent sort problem
2008-12-17, by haftmann
merged.
2008-12-16, by huffman
new theory Dsum: cpo of disjoint sum
2008-12-16, by huffman
scale dependency graph in document
2008-12-16, by huffman
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-16, by Christian Urban
proper document antiquotations;
2008-12-16, by wenzelm
merged
2008-12-16, by wenzelm
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-12-16, by krauss
future proofs: Future.fork_pri 1 minimizes queue length and pending promises
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
Future.fork_pri;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
removed old scheduler;
2008-12-16, by wenzelm
tuned enqueue: plain add_edge, acyclic not required here;
2008-12-16, by wenzelm
tuned messages;
2008-12-15, by wenzelm
updated generated file;
2008-12-15, by wenzelm
repaired railroad accident;
2008-12-15, by wenzelm
updated generated files;
2008-12-15, by wenzelm
added 'atp_messages' command, which displays recent messages synchronously;
2008-12-15, by wenzelm
merged
2008-12-15, by nipkow
flipped fold implementation
2008-12-15, by nipkow
merged
2008-12-11, by nipkow
codegen
2008-12-11, by nipkow
code for {x:A. P(x)} and for fold
2008-12-11, by nipkow
Testfile for Stefan's code generator
2008-12-11, by nipkow
moved value.ML to src/Tools
2008-12-15, by haftmann
\underscoreoff is now default
2008-12-15, by haftmann
tuned some proofs
2008-12-15, by Christian Urban
removed Ids;
2008-12-13, by wenzelm
merged
2008-12-13, by berghofe
merged
2008-12-13, by berghofe
merged
2008-12-13, by berghofe
Unified syntax of nominal_primrec with the one used by fun(ction) and new
2008-12-13, by berghofe
Modified nominal_primrec to make it work with local theories, unified syntax
2008-12-13, by berghofe
merged
2008-12-13, by wenzelm
tuned comments;
2008-12-13, by wenzelm
tuned ML_OPTIONS for improved multicore performance;
2008-12-13, by wenzelm
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
2008-12-13, by wenzelm
requires: check ancestors directly;
2008-12-13, by wenzelm
Context.display_names;
2008-12-13, by wenzelm
global_qed: refrain from ProofContext.auto_bind_facts, to avoid
2008-12-12, by wenzelm
usage: echo ML settings as well;
2008-12-13, by wenzelm
future proofs: more robust check via Future.enabled;
2008-12-12, by wenzelm
removed former Isabelle font (cf. IsabelleItalic);
2008-12-11, by wenzelm
incorporated isabelle-fonts side-branch (forced merge);
2008-12-11, by wenzelm
replaced single quote by mathematical prime;
2008-09-06, by wenzelm
generated file;
2008-08-24, by wenzelm
bold version: math glyphs from plain IsabelleMono;
2008-08-24, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip