isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

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