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.
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
2009-01-10, by wenzelm
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
2009-01-10, by wenzelm
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10, by wenzelm
remove_thy: perform PureThy.cancel_proofs;
2009-01-10, by wenzelm
added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10, by wenzelm
added pending_groups -- accumulates task groups of local derivations only;
2009-01-10, by wenzelm
added cancel_group;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
schedule_futures: tuned final consolidation, explicit after_load phase;
2009-01-10, by wenzelm
load_thy: explicit after_load phase for presentation;
2009-01-10, by wenzelm
excursion: commit_exit internally -- checkpoints are fully persistent now;
2009-01-10, by wenzelm
slightly more robust matching of session name;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
fixed proof involving dvd;
2009-01-10, by wenzelm
tuned;
2009-01-10, by wenzelm
added force_result;
2009-01-10, by wenzelm
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
2009-01-10, by wenzelm
simplified join_proofs;
2009-01-10, by wenzelm
merged
2009-01-09, by wenzelm
added split_thy_path;
2009-01-09, by wenzelm
added running task markup;
2009-01-09, by wenzelm
tuned;
2009-01-08, by wenzelm
merged
2009-01-08, by wenzelm
merged
2009-01-09, by wenzelm
merged.
2009-01-09, by huffman
fix proof broken by changes in dvd theory
2009-01-09, by huffman
merged.
2009-01-08, by huffman
remove type-specific proofs
2009-01-08, by huffman
add lemma dvd_diff to class comm_ring_1
2009-01-08, by huffman
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
2009-01-08, by huffman
move lemmas mult_minus{left,right} inside class ring
2009-01-08, by huffman
clean up division_ring proofs
2009-01-08, by huffman
add class ring_div; generalize mod/diff/minus proofs for class ring_div
2009-01-08, by huffman
generalize zmod_zmod_cancel -> mod_mod_cancel
2009-01-08, by huffman
generalize some div/mod lemmas; remove type-specific proofs
2009-01-08, by huffman
add tracing for domain package proofs
2009-01-07, by huffman
rename abbreviation square -> power2, to match theorem names
2009-01-06, by huffman
merged
2009-01-09, by haftmann
split of Imperative_HOL theories from HOL-Library
2009-01-08, by haftmann
NEWS and CONTRIBUTORS
2009-01-08, by haftmann
dded code_thm antiquotation
2009-01-08, by haftmann
made SML/NJ happy
2009-01-08, by haftmann
merged
2009-01-07, by wenzelm
merged
2009-01-07, by haftmann
tuned siganture of locale.ML
2009-01-07, by haftmann
tuned signature; internal code reorganisation
2009-01-07, by haftmann
tuned signature; changed locale predicate name convention
2009-01-07, by haftmann
changed locale predicate name convention
2009-01-07, by haftmann
inductive: added fork_mono flag;
2009-01-07, by wenzelm
added fork_mono flag, which is usually enabled in batch-mode only;
2009-01-07, by wenzelm
Proof.global_future_terminal_proof;
2009-01-07, by wenzelm
Proof.global_future_proof;
2009-01-07, by wenzelm
future_proof: refined version covers local_future_proof and global_future_proof;
2009-01-07, by wenzelm
more robust propagation of errors through bulk jobs;
2009-01-07, by wenzelm
qed/after_qed: singleton result;
2009-01-07, by wenzelm
Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;
2009-01-07, by wenzelm
future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-07, by wenzelm
added local_theory';
2009-01-07, by wenzelm
merged
2009-01-07, by haftmann
proper local_theory after Class.class
2009-01-07, by haftmann
more parallel loading;
2009-01-06, by wenzelm
more parallel loading;
2009-01-06, by wenzelm
merged
2009-01-06, by wenzelm
merged.
2009-01-06, by huffman
make cont_proc handle eta-contracted terms
2009-01-06, by huffman
implement is_closed_term using Term.loose_bvar
2009-01-06, by huffman
use Thm.close_derivation instead of standard
2009-01-05, by huffman
tuned;
2009-01-06, by wenzelm
merged
2009-01-06, by wenzelm
renamed structure ParList to Par_List;
2009-01-06, by wenzelm
parallelized merge_data;
2009-01-06, by wenzelm
tuned map: reduced overhead due to bulk jobs;
2009-01-06, by wenzelm
added is_valid;
2009-01-06, by wenzelm
future_terminal_proof: check Future.enabled;
2009-01-06, by wenzelm
merged
2009-01-06, by haftmann
locale -> old_locale, new_locale -> locale
2009-01-06, by haftmann
locale -> old_locale, new_locale -> locale
2009-01-05, by haftmann
locale -> old_locale, new_locale -> locale
2009-01-05, by haftmann
removed locale adaption layer
2009-01-05, by haftmann
rearranged target theories
2009-01-05, by haftmann
removed locale adaption layer
2009-01-05, by haftmann
merged
2009-01-05, by wenzelm
misc tuning and modernization;
2009-01-05, by wenzelm
merged.
2009-01-05, by huffman
add lemma psize_unique; simplify some proofs
2008-12-29, by huffman
minimize imports
2008-12-29, by huffman
parallelize some internal proofs via Proof.future_terminal_proof;
2009-01-05, by wenzelm
added future_terminal_proof;
2009-01-05, by wenzelm
Isar.init;
2009-01-05, by wenzelm
simplified tty model -- back to plain list history, which is independent of editor model;
2009-01-05, by wenzelm
added is_control, is_regular, is_theory_begin;
2009-01-05, by wenzelm
more precise is_relevant: requires original main goal, not initial goal state;
2009-01-04, by wenzelm
tuned protect, conclude: Drule.comp_no_flatten;
2009-01-04, by wenzelm
added comp_no_flatten;
2009-01-04, by wenzelm
future proofs: back to Future.fork_pri ~1 for improved parallelism;
2009-01-04, by wenzelm
cancel: unique threads;
2009-01-04, by wenzelm
more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;
2009-01-03, by wenzelm
added eq_group;
2009-01-03, by wenzelm
merged
2009-01-03, by haftmann
separator, is_qualified
2009-01-03, by haftmann
added instance for bot, top
2009-01-03, by haftmann
added binding.ML
2009-01-03, by haftmann
merged
2009-01-02, by haftmann
merged
2009-01-02, by haftmann
improved boostrap order: theory_target.ML before expression.ML
2009-01-02, by haftmann
named code theorem for Fract_norm
2009-01-02, by haftmann
tuned settings;
2009-01-02, by wenzelm
merged
2009-01-02, by wenzelm
removed references to OldTerm.*
2009-01-02, by krauss
tuned message_text;
2009-01-02, by wenzelm
removed obsolete XML mode;
2009-01-02, by wenzelm
xsymbols: use plain Symbol.output;
2009-01-02, by wenzelm
Markup.no_output;
2009-01-02, by wenzelm
added output;
2009-01-02, by wenzelm
removed unused add_substring;
2009-01-02, by wenzelm
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
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip