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.
Interpretation in theories including interaction with subclass relation.
2008-12-05, by ballarin
merged
2008-12-05, by haftmann
dropped NameSpace.declare_base
2008-12-05, by haftmann
fix proofs
2008-12-04, by huffman
merged.
2008-12-04, by huffman
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
2008-12-04, by huffman
remove duplicated lemmas
2008-12-04, by huffman
include iszero_simps in lemmas comp_arith
2008-12-04, by huffman
add named lemma lists: neg_simps and iszero_simps
2008-12-04, by huffman
change arith_special simps to avoid using neg
2008-12-04, by huffman
merged
2008-12-05, by kleing
run test for sunbroy2 on /tmp,
2008-12-05, by kleing
merged
2008-12-05, by wenzelm
refined Future.fork interfaces, no longer export Future.future;
2008-12-04, by wenzelm
fork/map: no inheritance of group (structure is nested, not parallel);
2008-12-04, by wenzelm
future proofs: pass actual futures to facilitate composite computations;
2008-12-04, by wenzelm
renamed type Lazy.T to lazy;
2008-12-04, by wenzelm
future_scheduler: no global task group, exceptions via collective join;
2008-12-04, by wenzelm
renamed type Lazy.T to lazy;
2008-12-04, by wenzelm
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
2008-12-04, by wenzelm
future proofs: pass actual futures to facilitate composite computations;
2008-12-04, by wenzelm
renamed type Future.T to future;
2008-12-04, by wenzelm
renamed type Lazy.T to lazy;
2008-12-04, by wenzelm
merged.
2008-12-04, by huffman
change more lemmas to avoid using iszero
2008-12-04, by huffman
change some lemmas to avoid using iszero
2008-12-03, by huffman
enable eq_bin_simps for simplifying equalities on numerals
2008-12-03, by huffman
merged
2008-12-04, by haftmann
cleaned up binding module and related code
2008-12-04, by haftmann
NEWS
2008-12-04, by nipkow
fix proofs related to simplification of inequalities on numerals
2008-12-03, by huffman
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
2008-12-03, by huffman
simplify proof of less_nat_number_of
2008-12-03, by huffman
merged.
2008-12-03, by huffman
fixed proofs due to changes in Int.thy
2008-12-03, by huffman
cleaned up subsection headings;
2008-12-03, by huffman
sources are not executable;
2008-12-03, by wenzelm
eliminated traces of old Distribution directory;
2008-12-03, by wenzelm
merged
2008-12-03, by wenzelm
remove *.lof as well;
2008-12-03, by wenzelm
merged
2008-12-03, by haftmann
made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-12-03, by haftmann
Sublocale: removed public after_qed; identifiers private to NewLocale.
2008-12-03, by ballarin
Made global_note_qualified public.
2008-12-03, by ballarin
more examples
2008-12-03, by webertj
fixed typo
2008-12-03, by haftmann
unfold_locales is default method - no need for explicit references
2008-12-03, by haftmann
Automated merge with file:///mnt/home/isabelle-repository/repos/isabelle
2008-12-02, by wenzelm
Corrected imports.
2008-12-02, by berghofe
clean up imports related to ContNotDenum
2008-12-01, by huffman
ignore aux stuff in doc-src;
2008-12-01, by wenzelm
merged
2008-12-01, by haftmann
new Binding module
2008-12-01, by haftmann
Locale.*note* with conventional argument type
2008-12-01, by haftmann
added code equation for subset
2008-12-01, by haftmann
Merged again.
2008-12-01, by ballarin
Merged.
2008-12-01, by ballarin
No resolution of patterns within context statements.
2008-12-01, by ballarin
removed CVS Id;
2008-12-02, by wenzelm
proper check of ISABELLE_TOOLS directories;
2008-12-01, by wenzelm
removed obsolete tags (leftover from old CVS branches);
2008-12-01, by wenzelm
makedist -- make Isabelle source distribution (Mercurial version);
2008-12-01, by wenzelm
renamed makedist_mercurial to makedist, deleting the old version;
2008-12-01, by wenzelm
updated to python2.5;
2008-12-01, by wenzelm
convert to isabelle-cvs, the old version;
2008-12-01, by wenzelm
adapted description: old CVS;
2008-12-01, by wenzelm
Methods intro_locales and unfold_locales apply to both old and new locales.
2008-12-01, by ballarin
code_include with attach
2008-12-01, by haftmann
experimental implementation of a well-sorting algorithm
2008-12-01, by haftmann
code_funcgr interface includes also sort algebra
2008-12-01, by haftmann
exported get_accesses (for diagnostic purpose)
2008-12-01, by haftmann
more means for algebra projection
2008-12-01, by haftmann
consider TeX spacing conventions for punctuation marks
2008-12-01, by haftmann
fix typed print translation for card UNIV
2008-11-30, by huffman
removed obsolete CVS instructions;
2008-11-30, by wenzelm
fixed spelling;
2008-11-30, by wenzelm
tuned;
2008-11-30, by wenzelm
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
2008-11-30, by wenzelm
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
2008-11-30, by wenzelm
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
2008-11-30, by wenzelm
misc tuning and clarification;
2008-11-30, by wenzelm
remove repository-only files;
2008-11-29, by wenzelm
more .hgignore entries;
2008-11-29, by wenzelm
tuned;
2008-11-29, by wenzelm
basic setup of .hgignore;
2008-11-29, by wenzelm
further notes;
2008-11-29, by wenzelm
Important notes on Mercurial repository access for Isabelle.
2008-11-29, by wenzelm
Floats for Real.
2008-11-29, by nipkow
new file float_syntax.ML
2008-11-29, by nipkow
New lexical item "float".
2008-11-29, by nipkow
Intro_locales_tac to simplify goals involving locale predicates.
2008-11-28, by ballarin
Ahere to modern naming conventions; proper treatment of internal vs external names.
2008-11-28, by ballarin
added Tim's find_theorems performance patch
2008-11-28, by kleing
FindTheorems performance improvements (from Timothy Bourke)
2008-11-28, by kleing
Perform higher-order pattern matching during round-up.
2008-11-28, by ballarin
Proper treatment of expressions with free arguments.
2008-11-27, by ballarin
Roundup bound.
2008-11-27, by ballarin
Tests for sublocale command.
2008-11-27, by ballarin
Sublocale command.
2008-11-27, by ballarin
Command to add dependencies, fixed processing of dependencies.
2008-11-27, by ballarin
Fixed strange indentation.
2008-11-27, by ballarin
add Algebraic and Universal to imports
2008-11-25, by huffman
separate run and cases combinators
2008-11-25, by huffman
renamed lemma compact_minimal to compact_bot_minimal;
2008-11-25, by huffman
renamed lemma compact_minimal to compact_bot_minimal
2008-11-25, by huffman
Use standard export function.
2008-11-25, by ballarin
Expression types cleaned up.
2008-11-25, by ballarin
Test for term patterns added.
2008-11-25, by ballarin
Expression types cleaned up, proper treatment of term patterns.
2008-11-25, by ballarin
check for more common errors first
2008-11-24, by krauss
improved error msg; tuned
2008-11-24, by krauss
removed "log" again, as IntInf.log2 already exists.
2008-11-24, by krauss
Some regression tests for theorem statements.
2008-11-24, by ballarin
Enable switching to new locales during session.
2008-11-24, by ballarin
Read/cert_statement for theorem statements.
2008-11-24, by ballarin
Generalised activation code.
2008-11-24, by ballarin
More ramifications of removal of 'includes' element.
2008-11-24, by ballarin
tuned;
2008-11-23, by wenzelm
eliminated finish_proof, keep pre/post normalization of results separate;
2008-11-23, by wenzelm
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
2008-11-23, by wenzelm
Regression tests for new locale implementation.
2008-11-21, by ballarin
add_locale functional.
2008-11-21, by ballarin
Added a line that was missing from the definition
2008-11-21, by paulson
added binary logarithm
2008-11-21, by krauss
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
2008-11-21, by paulson
Name.binding
2008-11-21, by haftmann
added optimizer
2008-11-20, by nipkow
reactivated some dead theories (based on hints by Mark Hillebrand);
2008-11-20, by wenzelm
Locale.local_note_qualified
2008-11-20, by haftmann
fact table now using name bindings
2008-11-20, by haftmann
dropped legacy naming code
2008-11-20, by haftmann
tuned name bindings
2008-11-20, by haftmann
using name bindings
2008-11-20, by haftmann
name spaces and name bindings
2008-11-20, by haftmann
Deleted debug message (PolyML).
2008-11-20, by ballarin
removed traces of former 'includes' element;
2008-11-20, by wenzelm
updated generated files;
2008-11-20, by wenzelm
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-20, by wenzelm
*** empty log message ***
2008-11-19, by nipkow
fixed
2008-11-19, by nipkow
Added new fold operator and renamed the old oe to fold_image.
2008-11-19, by nipkow
Type inference for elements through syntax module.
2008-11-19, by ballarin
Use 'if' in connection with 'is_some' and 'the'.
2008-11-19, by ballarin
Basic types not qualified.
2008-11-19, by ballarin
Enable switching to new locales during session.
2008-11-19, by ballarin
explicit inhabitance proof
2008-11-19, by haftmann
fulfill_proof/thm_proof: commuted lazyness;
2008-11-18, by wenzelm
fulfill_proof/thm_proof: commuted lazyness;
2008-11-18, by wenzelm
removed lemmas called lemma1 and lemma2
2008-11-18, by krauss
force_proofs after cumulative use_thys;
2008-11-18, by wenzelm
signed_string_of_int for priorities;
2008-11-18, by wenzelm
added force_proofs;
2008-11-18, by wenzelm
added force_proofs (based on thms ever passed through enter_thms);
2008-11-18, by wenzelm
tuned;
2008-11-18, by wenzelm
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
2008-11-18, by wenzelm
moved table of standard Isabelle symbols to isar-ref manual;
2008-11-18, by wenzelm
added isabelle-implementation manual;
2008-11-18, by wenzelm
disabled threads -- as advertized;
2008-11-18, by wenzelm
changes by Fabian Immler:
2008-11-18, by wenzelm
Code for switching to new locales.
2008-11-18, by ballarin
add_thmss
2008-11-18, by ballarin
Activate elements moved to element.ML.
2008-11-18, by ballarin
finish: force proofs;
2008-11-18, by wenzelm
finish_proof: undefined promises may occur here;
2008-11-17, by wenzelm
tuned promise/fullfill;
2008-11-17, by wenzelm
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
2008-11-17, by wenzelm
removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-17, by wenzelm
simplified thm_deps -- no need to build a graph datastructure;
2008-11-17, by wenzelm
removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-17, by wenzelm
-> AFP
2008-11-17, by nipkow
tuned unfold_locales invocation
2008-11-17, by haftmann
explicit name morphism function for locale interpretation
2008-11-17, by haftmann
Name.name_with_prefix (temporarily)
2008-11-17, by haftmann
adjusted locale signature to *_cmd convention
2008-11-17, by haftmann
whitespace tuning
2008-11-17, by haftmann
Generic activation of locales.
2008-11-17, by ballarin
proof_body/pthm: removed redundant types field;
2008-11-16, by wenzelm
put_name/thm_proof: promises are filled with fulfilled proofs;
2008-11-16, by wenzelm
proof_body/pthm: removed redundant types field;
2008-11-16, by wenzelm
clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-16, by wenzelm
- Corrected order of quantification over Frees.
2008-11-16, by berghofe
Frees in PThms are now quantified in the order of their appearance in the
2008-11-16, by berghofe
adapted PThm and MinProof;
2008-11-15, by wenzelm
retrieve thm deps from proof_body;
2008-11-15, by wenzelm
retrieve thm deps from proof_body;
2008-11-15, by wenzelm
adapted PThm;
2008-11-15, by wenzelm
proof_of_term: removed obsolete disambiguisation table;
2008-11-15, by wenzelm
rewrite_proof: simplified simprocs (no name required);
2008-11-15, by wenzelm
Thm.proof_of returns proof_body;
2008-11-15, by wenzelm
refined notion of derivation, consiting of promises and proof_body;
2008-11-15, by wenzelm
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
2008-11-15, by wenzelm
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-11-15, by wenzelm
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
2008-11-15, by wenzelm
name_of_thm: Proofterm.fold_proof_atoms;
2008-11-15, by wenzelm
Thm.proof_of returns proof_body;
2008-11-15, by wenzelm
clean: added HOL-Main;
2008-11-15, by wenzelm
rewrite_proof: simplified simprocs (no name required);
2008-11-15, by wenzelm
multithreading support for polyml-5.2 actually disabled -- as advertized;
2008-11-15, by wenzelm
Initial part of locale reimplementation.
2008-11-14, by ballarin
Made local_note_prefix public.
2008-11-14, by ballarin
re-educated guess
2008-11-14, by haftmann
namify and name_decl combinators
2008-11-14, by haftmann
Name.is_nothing
2008-11-14, by haftmann
lemmas about dom and minus / insert
2008-11-14, by haftmann
added length_unique operation for code generation
2008-11-14, by haftmann
updated generated files;
2008-11-13, by wenzelm
removed "includes" element (lost update?);
2008-11-13, by wenzelm
updated generated files;
2008-11-13, by wenzelm
added section "Explicit instantiation within a subgoal context";
2008-11-13, by wenzelm
renamed "Rules" to "Object-level rules";
2008-11-13, by wenzelm
more on basic tactics;
2008-11-13, by wenzelm
basic ML reference for tactics;
2008-11-13, by wenzelm
added section "Tactics";
2008-11-13, by wenzelm
more contributors;
2008-11-13, by wenzelm
separate section "Inspecting the syntax" for print_syntax;
2008-11-13, by wenzelm
misc tuning of inner syntax;
2008-11-13, by wenzelm
added inner lexical syntax, reusing outer one;
2008-11-13, by wenzelm
misc tuning;
2008-11-13, by wenzelm
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
2008-11-13, by wenzelm
more tuning of Pure grammer;
2008-11-13, by wenzelm
updated and elaborated Pure grammer;
2008-11-13, by wenzelm
added Pure grammer (from old ref manual);
2008-11-13, by wenzelm
mixfix annotations: verbatim for special symbols;
2008-11-13, by wenzelm
added section "The Pure grammar" (incomplete version, based on old ref manual);
2008-11-13, by wenzelm
added section "Priority grammars" (variant from old ref manual);
2008-11-13, by wenzelm
added section "Co-regularity of type classes and arities" (variant from old ref manual);
2008-11-13, by wenzelm
minor tuning (according to old ref manual);
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
fixed/tuned syntax for attribute "tagged";
2008-11-13, by wenzelm
added pretty printing options (from old ref manual);
2008-11-13, by wenzelm
separate chapter "Inner syntax --- the term language";
2008-11-13, by wenzelm
updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13, by wenzelm
unified use of declaration environment with IsarImplementation;
2008-11-13, by wenzelm
ignore ThyOutput.source flag;
2008-11-13, by wenzelm
added bind_thm, bind_thms;
2008-11-13, by wenzelm
tuned section "Incorporating ML code";
2008-11-13, by wenzelm
tuned section "Oracles";
2008-11-13, by wenzelm
tuned section arrangement;
2008-11-13, by wenzelm
moved section "Proof method expressions" to proof chapter;
2008-11-13, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip