Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-1920
+1920
+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.
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
fixed rangle;
2008-08-24, by wenzelm
use dash from text font, not math;
2008-08-24, by wenzelm
added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak);
2008-08-24, by wenzelm
generated ttf;
2008-08-22, by wenzelm
renamed to IsabelleMono;
2008-08-22, by wenzelm
added README with original licenses;
2008-08-22, by wenzelm
renamed Isabelle to IsabelleItalic;
2008-08-22, by wenzelm
fixed rangle glyph;
2008-08-22, by wenzelm
the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
2008-08-22, by wenzelm
Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
2008-08-22, by wenzelm
Isabelle font, based on TeX glyhps;
2008-08-22, by wenzelm
enable future_scheduler by default;
2008-12-11, by wenzelm
ISABELLE_USEDIR_OPTIONS: -M max is default;
2008-12-11, by wenzelm
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
2008-12-11, by wenzelm
removed spurious exception_trace;
2008-12-11, by wenzelm
print_theorems: more robust difference, even after finished proof;
2008-12-11, by wenzelm
export context_node;
2008-12-11, by wenzelm
merged
2008-12-11, by wenzelm
more antiquotations;
2008-12-10, by wenzelm
pcpodef package: state two goals, instead of encoded conjunction;
2008-12-11, by wenzelm
recovered goal_pat;
2008-12-11, by wenzelm
inhabitance goal is now stated in original form and result contracted --
2008-12-11, by wenzelm
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
2008-12-11, by wenzelm
add_typedef: unfold set_def in tactical proof as well;
2008-12-11, by wenzelm
merged
2008-12-11, by wenzelm
Theory.checkpoint before commencing proof;
2008-12-11, by wenzelm
misc tuning and modernisation;
2008-12-11, by wenzelm
merged
2008-12-10, by wenzelm
logically separate typedef axiomatization from constant definition
2008-12-08, by krauss
add def before setting up goal
2008-12-08, by krauss
killed dead code
2008-12-07, by krauss
constrain type inference to sort "type"
2008-12-11, by krauss
merged.
2008-12-10, by huffman
cleaned up some proofs in Cfun.thy
2008-12-10, by huffman
implement cont_proc theorem cache using theory data
2008-12-10, by huffman
use ML antiquotations
2008-12-10, by huffman
clean up diff_bin_simps
2008-12-10, by huffman
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
2008-12-10, by huffman
fixed import: requires ContNotDenum;
2008-12-10, by wenzelm
fixed import: requires ContNotDenum;
2008-12-10, by wenzelm
requires RComplete;
2008-12-10, by wenzelm
merged.
2008-12-10, by huffman
move all neg-related lemmas to NatBin; make type of neg specific to int
2008-12-09, by huffman
separate neg_simps from rel_simps
2008-12-09, by huffman
use {less,le}_number_of in integer simprocs
2008-12-09, by huffman
use lemma lists defined in Int.thy
2008-12-09, by huffman
Merged.
2008-12-10, by ballarin
Satisfy a_axioms.
2008-12-10, by ballarin
Merged.
2008-12-10, by ballarin
Enable keyword 'structure' in for clause of locale expression.
2008-12-10, by ballarin
Correct order of defines in specification.
2008-12-09, by ballarin
Pass on defines in inheritance; reject illicit defines created by instantiation.
2008-12-09, by ballarin
Order of implicit parameters in locale expression.
2008-12-09, by ballarin
NewLocale.intro_locales_tac added to Class.default_intro_tac.
2008-12-09, by ballarin
When adding locales, delay notes until local theory is built.
2008-12-09, by ballarin
merged
2008-12-10, by nipkow
moved ContNotDenum into Library
2008-12-10, by nipkow
move lemmas from Numeral_Type.thy to other theories
2008-12-09, by huffman
instantiation option :: (enum) enum
2008-12-09, by huffman
instance inat :: semiring_char_0
2008-12-09, by huffman
Default names for definitions.
2008-12-08, by ballarin
Proper shape of assumptions generated from Defines elements.
2008-12-08, by ballarin
Merged.
2008-12-08, by ballarin
Explicitly close up defines.
2008-12-08, by ballarin
Interpretation in proof contexts.
2008-12-05, by ballarin
tuned LaTeX files
2008-12-08, by haftmann
tuned LaTeX files
2008-12-08, by haftmann
merged.
2008-12-06, by huffman
multiplication for type inat
2008-12-06, by huffman
fix proofs
2008-12-06, by huffman
change lemmas to avoid using neg
2008-12-06, by huffman
simplify less_nat_number_of
2008-12-05, by huffman
add lemma le_nat_number_of
2008-12-05, by huffman
merged
2008-12-06, by wenzelm
adapted to changes in binding module
2008-12-06, by haftmann
merged
2008-12-06, by haftmann
Name.name_of -> Binding.base_name
2008-12-05, by haftmann
corrected theory path
2008-12-05, by haftmann
removed Table.extend, NameSpace.extend_table
2008-12-05, by haftmann
renamed force_proof to join_proof;
2008-12-06, by wenzelm
renamed force_proofs to join_proofs;
2008-12-06, by wenzelm
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
2008-12-06, by wenzelm
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
2008-12-06, by wenzelm
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
2008-12-06, by wenzelm
added new_task;
2008-12-06, by wenzelm
added constant value;
2008-12-06, by wenzelm
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
2008-12-05, by wenzelm
uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;
2008-12-05, by wenzelm
Merged.
2008-12-05, by ballarin
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
more on mixfix annotations (updated material from old ref manual);
2008-11-13, by wenzelm
tuned;
2008-11-13, by wenzelm
moved section "Document preparation" to front;
2008-11-13, by wenzelm
updated section "Markup via command tags";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
tuned "Markup commands";
2008-11-13, by wenzelm
tuned intro of "Document preparation";
2008-11-13, by wenzelm
reworked "Defining Theories";
2008-11-13, by wenzelm
removed Assert.thy
2008-11-13, by haftmann
dropped superfluos eval_conv
2008-11-13, by haftmann
moved assert to Heap_Monad.thy
2008-11-13, by haftmann
simproc for let
2008-11-13, by haftmann
improved handling of !!/==> for eval and normalization
2008-11-13, by haftmann
proper name morphisms for locales
2008-11-13, by haftmann
consider prefixes for name bindings of simprocs (a first approximation)
2008-11-13, by haftmann
diagnostic output for name bindings
2008-11-13, by haftmann
Some modifications in code for proving arities to make it work for datatype
2008-11-13, by berghofe
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
2008-11-12, by krauss
restruced naming code in anticipation of introduction of name morphisms
2008-11-10, by haftmann
more verbose element printing
2008-11-10, by haftmann
clarified comment
2008-11-10, by haftmann
Added support for parametric datatypes.
2008-11-10, by berghofe
Streamlined functions for accessing information about atoms.
2008-11-10, by berghofe
Some more functions for accessing information about atoms.
2008-11-10, by berghofe
Made doc compatible with the system.
2008-11-10, by ballarin
clarified verbatim vs. typewriter
2008-11-10, by haftmann
using explicit interpretaton prefix in Name.binding (still on the surface)
2008-11-10, by haftmann
explicit interpretation prefix in Name.binding
2008-11-10, by haftmann
tuned
2008-11-10, by haftmann
exported codegen_preproc
2008-11-07, by haftmann
Minor cleanup.
2008-11-06, by ballarin
Keyword 'includes' gone.
2008-11-06, by ballarin
tuned
2008-11-06, by nipkow
added lemma
2008-11-06, by nipkow
Added second tiling example.
2008-11-06, by nipkow
cleaned
2008-11-06, by haftmann
tuned
2008-11-06, by haftmann
class morphism stemming from locale interpretation
2008-11-06, by haftmann
improved verbatim mechanism
2008-11-03, by haftmann
Theorem "_" is now stored with open derivation.
2008-10-31, by berghofe
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
2008-10-31, by berghofe
Replaced arbitrary by undefined.
2008-10-31, by berghofe
Dropped context element 'includes'.
2008-10-30, by ballarin
adapted to strict pattern discipline
2008-10-29, by haftmann
explicit check for pattern discipline before code translation
2008-10-29, by haftmann
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-28, by ballarin
restored incremental code generation
2008-10-28, by haftmann
slightly tuned
2008-10-28, by haftmann
assert that no class parameter is used as constructor
2008-10-28, by haftmann
cleanup code default attribute
2008-10-28, by haftmann
removed includes
2008-10-28, by haftmann
making SMLNJ happy
2008-10-28, by haftmann
The metis method no longer fails because the theorem is too trivial
2008-10-28, by paulson
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-10-28, by ballarin
metis proof
2008-10-27, by paulson
New-style locale expressions with instantiation (new file expression.ML).
2008-10-27, by ballarin
Hide path in constant name (workaround).
2008-10-27, by ballarin
explicit history for equations; tuned
2008-10-27, by haftmann
slightly tuned
2008-10-27, by haftmann
added rudimentary code generation
2008-10-27, by haftmann
sup_bot and inf_top
2008-10-27, by haftmann
Extension of interface: declarations_of.
2008-10-27, by ballarin
simplified user-defined class syntax
2008-10-24, by haftmann
more clever module names for code generation
2008-10-24, by haftmann
"fun" gained a more uniform status
2008-10-24, by haftmann
simplified syntax for class parameters
2008-10-24, by haftmann
tuned
2008-10-24, by haftmann
new classes "top" and "bot"
2008-10-24, by haftmann
tuned proof
2008-10-24, by haftmann
more clever module name aliasses for code generation
2008-10-24, by haftmann
"arbitrary" merely abbreviates undefined
2008-10-24, by haftmann
subst is a proper axiom again
2008-10-24, by haftmann
updated
2008-10-24, by haftmann
explicit namings for generated code
2008-10-24, by haftmann
Thm.get_def;
2008-10-23, by wenzelm
Thm.def_name;
2008-10-23, by wenzelm
multithreading support only for polyml-5.2.1 or later;
2008-10-23, by wenzelm
renamed get_axiom_i to axiom, removed obsolete get_axiom;
2008-10-23, by wenzelm
renamed Thm.get_axiom_i to Thm.axiom;
2008-10-23, by wenzelm
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
2008-10-23, by wenzelm
adapted Susp.peek;
2008-10-23, by wenzelm
thread-safe version, with non-critical evaluation;
2008-10-23, by wenzelm
do not open Susp;
2008-10-23, by wenzelm
switched parallel sessions to polyml-5.2.1;
2008-10-23, by wenzelm
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
2008-10-23, by wenzelm
updated to 5.2.1;
2008-10-22, by wenzelm
prove_instantiation_exit combinators
2008-10-22, by haftmann
added meet_sort_typ
2008-10-22, by haftmann
tuned
2008-10-22, by haftmann
code identifier namings are no longer imperative
2008-10-22, by haftmann
tuned typedef interface
2008-10-22, by haftmann
slightly tuned
2008-10-22, by haftmann
fixed
2008-10-22, by haftmann
less ambitious default for JEDIT_JAVA_OPTIONS;
2008-10-21, by wenzelm
JEDIT_OPTIONS: moved -settings to interface script (more robust);
2008-10-21, by wenzelm
make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
2008-10-21, by wenzelm
Added nominal_inductive2.
2008-10-21, by berghofe
Example for using the generalized version of nominal_inductive.
2008-10-21, by berghofe
Added theory W.
2008-10-21, by berghofe
More general, still experimental version of nominal_inductive for
2008-10-21, by berghofe
Added nominal_inductive2.ML
2008-10-21, by berghofe
added jEdit settings;
2008-10-21, by wenzelm
tuned usage line;
2008-10-21, by wenzelm
Isabelle/jEdit interface wrapper.
2008-10-21, by wenzelm
join results in isolation;
2008-10-21, by wenzelm
join_results: allow CRITICAL join of finished futures;
2008-10-21, by wenzelm
Future.join_result;
2008-10-21, by wenzelm
added Future.enabled check;
2008-10-21, by wenzelm
ThyOutput: export some auxiliary operations;
2008-10-21, by wenzelm
fixed proof
2008-10-20, by nipkow
added lemmas
2008-10-20, by nipkow
Names of variables in perm_eqs are now chosen more carefully to avoid
2008-10-19, by berghofe
- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
2008-10-19, by berghofe
datatype_codegen now checks name of result type of constructor
2008-10-19, by berghofe
run a program in a modified environment;
2008-10-19, by wenzelm
reactivated HOL-Matrix;
2008-10-17, by wenzelm
tuned
2008-10-17, by haftmann
filled remaining gaps
2008-10-17, by haftmann
added type antiquotation
2008-10-17, by haftmann
tuned;
2008-10-16, by wenzelm
added dep for Concurrent/ROOT.ML;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
removed Locales;
2008-10-16, by wenzelm
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16, by wenzelm
added translations for SORT_CONSTRAINT
2008-10-16, by wenzelm
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added make;
2008-10-16, by wenzelm
maintain sort occurrences of declared terms;
2008-10-16, by wenzelm
added weaken_sorts;
2008-10-16, by wenzelm
added make, minimal_sorts;
2008-10-16, by wenzelm
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-10-16, by wenzelm
added check_shyps, which reject pending sort hypotheses;
2008-10-16, by wenzelm
Drule.norm_hhf_eqs;
2008-10-16, by wenzelm
prove_common: include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added rules for sort_constraint, include in norm_hhf_eqs;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
avoid accidental dependency of automated proof on sort equiv;
2008-10-16, by wenzelm
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
2008-10-16, by wenzelm
avoid CRITICAL with_path;
2008-10-16, by wenzelm
rewrite more proofs in Isar style
2008-10-16, by huffman
Removed ex/Locales.thy.
2008-10-16, by ballarin
More occurrences of 'includes' gone.
2008-10-16, by ballarin
Removed outdated locales tutorial.
2008-10-16, by ballarin
correct rounding
2008-10-16, by haftmann
circumvent some TeX problem
2008-10-16, by haftmann
only test HOL image for smlnj
2008-10-16, by kleing
tuned;
2008-10-15, by wenzelm
tuned;
2008-10-15, by wenzelm
generic ATP manager based on threads (by Fabian Immler);
2008-10-15, by wenzelm
added sledgehammer etc.;
2008-10-15, by wenzelm
removed obsolete Complex sessions;
2008-10-15, by wenzelm
figure for adaption
2008-10-15, by haftmann
Removed 'includes' (fixed).
2008-10-15, by ballarin
Removed 'includes'.
2008-10-15, by ballarin
give more time to do inital loggin and settings read
2008-10-15, by kleing
log start of test session
2008-10-15, by kleing
tuned interfaces -- plain prover function, without thread;
2008-10-14, by wenzelm
add_prover: plain prover function, without thread;
2008-10-14, by wenzelm
tuned AtpWrapper interfaces;
2008-10-14, by wenzelm
continued codegen tutorial
2008-10-14, by haftmann
renamed AtpThread to AtpWrapper;
2008-10-14, by wenzelm
adding preferences is now permissive;
2008-10-14, by wenzelm
tuned;
2008-10-14, by wenzelm
adding preferences is now permissive, no error handling here;
2008-10-14, by wenzelm
CRITICAL access to preferences;
2008-10-14, by wenzelm
export generic_pref etc.;
2008-10-14, by wenzelm
renamed kill_all to kill, in conformance with atp_kill command;
2008-10-14, by wenzelm
tuned comments;
2008-10-14, by wenzelm
added lemma
2008-10-14, by nipkow
Added liveness analysis
2008-10-14, by nipkow
info: back to plain printing;
2008-10-14, by wenzelm
added min_elem, upto;
2008-10-14, by wenzelm
added value;
2008-10-14, by wenzelm
simplified synchronized variable access;
2008-10-14, by wenzelm
State variables with synchronized access.
2008-10-13, by wenzelm
added generic combinator for synchronized evaluation (formerly in future.ML);
2008-10-13, by wenzelm
simplified implementation using Synchronized.var;
2008-10-13, by wenzelm
SimpleThread.synchronized;
2008-10-13, by wenzelm
added Concurrent/synchronized.ML;
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
tuned output;
2008-10-13, by wenzelm
tuned
2008-10-13, by haftmann
tuned
2008-10-13, by urbanc
change DISTPREFIX to not use yet another filesystem
2008-10-11, by kleing
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
`code func` now just `code`
2008-10-10, by haftmann
some adaption
2008-10-10, by haftmann
using tikz pictures
2008-10-10, by haftmann
tuned default rules of (dvd)
2008-10-10, by haftmann
replaced str_of by general peek;
2008-10-09, by wenzelm
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
2008-10-09, by wenzelm
fixed spelling;
2008-10-09, by wenzelm
added enabled;
2008-10-09, by wenzelm
added enabled;
2008-10-09, by wenzelm
Multithreading.enabled;
2008-10-09, by wenzelm
moved future_scheduler flag to Concurrent/ROOT.ML;
2008-10-09, by wenzelm
added invalidate_group;
2008-10-09, by wenzelm
added fail-safe interrupt;
2008-10-09, by wenzelm
subject to Multithreading.enabled;
2008-10-09, by wenzelm
future result: Interrupt invalidates group, but pretends success otherwise;
2008-10-09, by wenzelm
added future_scheduler flag (tmp!), from skip_proofs.ML;
2008-10-09, by wenzelm
Dummy version of parallel list combinators -- plain sequential evaluation.
2008-10-09, by wenzelm
added Concurrent/par_list_dummy.ML;
2008-10-09, by wenzelm
improved performance of skolem cache, due to parallel map;
2008-10-09, by wenzelm
SimpleThread.interrupt;
2008-10-09, by wenzelm
report: back to single message;
2008-10-09, by wenzelm
added section label;
2008-10-09, by wenzelm
tuned
2008-10-09, by haftmann
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
2008-10-09, by kleing
removed legacy |>>>
2008-10-09, by haftmann
established canonical argument order in SML code generators
2008-10-09, by haftmann
established canonical argument order
2008-10-09, by haftmann
made SMLNJ happy
2008-10-09, by haftmann
less tracing;
2008-10-08, by wenzelm
Future.joint_results is already uninterruptible;
2008-10-08, by wenzelm
more careful handling of group interrupts;
2008-10-08, by wenzelm
use polyml-cvs, which fixes a serious deadlock problem of Poly/ML runtime vs. GC;
2008-10-08, by wenzelm
added HOL-Main;
2008-10-08, by wenzelm
setmp_noncritical makes it work with future scheduler;
2008-10-08, by wenzelm
The result of the equality inference rule no longer undergoes factoring.
2008-10-08, by paulson
make the test for experimental sessions in isatest-check actually work
2008-10-08, by kleing
leave a log message when no snapshot is generated
2008-10-08, by kleing
clarified preprocessor policies
2008-10-07, by haftmann
arbitrary is undefined
2008-10-07, by haftmann
tuned whitespace
2008-10-07, by haftmann
only one theorem table for both code generators
2008-10-07, by haftmann
proper default codegen attribute
2008-10-07, by haftmann
tuned code setup
2008-10-07, by haftmann
code generator more liberal with respect to sort constraints of instance parameters
2008-10-07, by haftmann
more Isar for example
2008-10-07, by haftmann
tuned funpow code generation
2008-10-07, by haftmann
tuned min/max code generation
2008-10-07, by haftmann
dropped superfluous if
2008-10-07, by haftmann
tuned of_nat code generation
2008-10-07, by haftmann
re-introduces axiom subst
2008-10-07, by haftmann
corrected SML undefined
2008-10-07, by haftmann
updated to official version as of 07-Oct-2008;
2008-10-07, by wenzelm
fold_lines: more tuning, avoiding extra split_last;
2008-10-06, by wenzelm
extra check of PROOFGENERAL_HOME;
2008-10-06, by wenzelm
needs -b option for isabelle getenv
2008-10-05, by kleing
updated generated file;
2008-10-04, by wenzelm
tuned isabelle usage;
2008-10-04, by wenzelm
updated generated file;
2008-10-04, by wenzelm
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
2008-10-04, by wenzelm
updated generated file;
2008-10-04, by wenzelm
replaced ISABELLE by ISABELLE_PROCESS;
2008-10-04, by wenzelm
ISABELLE_PROCESS commandline;
2008-10-04, by wenzelm
replaced ISATOOL by ISABELLE_TOOL;
2008-10-04, by wenzelm
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);
2008-10-04, by wenzelm
eliminated prompt messages;
2008-10-04, by wenzelm
added isabelle_tool version as basic integrity check of platform/distribution;
2008-10-04, by wenzelm
renamed isatool to isabelle_tool in programming interfaces;
2008-10-04, by wenzelm
Theory header keywords.
2008-10-04, by wenzelm
added Thy/thy_header.scala;
2008-10-04, by wenzelm
tuned quotes;
2008-10-03, by wenzelm
factor: proper padding of digits;
2008-10-03, by wenzelm
plain process_id function;
2008-10-03, by wenzelm
removed obsolete Posix/Signal compatibility wrappers;
2008-10-03, by wenzelm
removed obsolete Posix/Signal compatibility wrappers;
2008-10-03, by wenzelm
removed obsolete Posix/Signal compatibility wrappers;
2008-10-03, by wenzelm
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
2008-10-03, by wenzelm
updated to new AtpManager;
2008-10-03, by wenzelm
operate on Proof.state, not Toplevel.state;
2008-10-03, by wenzelm
misc simplifcation and tuning;
2008-10-03, by wenzelm
perform atp_setups here;
2008-10-03, by wenzelm
updated generated file;
2008-10-03, by wenzelm
removed HOL-Plain -- already included in HOL;
2008-10-03, by wenzelm
removed spurious ResAtp.set_prover;
2008-10-03, by wenzelm
simplified thread creation via SimpleThread;
2008-10-03, by wenzelm
simplified thread creation via SimpleThread;
2008-10-03, by wenzelm
version of sledgehammer using threads instead of processes, misc cleanup;
2008-10-03, by wenzelm
removed old/unused setup of raw ATP oracles;
2008-10-03, by wenzelm
tuned;
2008-10-03, by wenzelm
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
2008-10-03, by wenzelm
added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;
2008-10-03, by wenzelm
tuned tracing;
2008-10-03, by wenzelm
slower heartbeat;
2008-10-03, by wenzelm
added simple heartbeat thread;
2008-10-02, by wenzelm
time factor: one more digit;
2008-10-02, by wenzelm
more tuning of tracing messages;
2008-10-02, by wenzelm
include factor in timing report;
2008-10-02, by wenzelm
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
2008-10-02, by wenzelm
tracing: ignore failure of any kind;
2008-10-02, by wenzelm
tuned SYNCHRONIZED: outermost Exn.release;
2008-10-02, by wenzelm
program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
2008-10-02, by wenzelm
added partiality section
2008-10-02, by haftmann
corrected class antiquotation
2008-10-02, by haftmann
max_threads_value always 1 for dummy version;
2008-10-02, by wenzelm
simplified Exn.EXCEPTIONS, flatten nested occurrences;
2008-10-02, by wenzelm
simplified Exn.EXCEPTIONS;
2008-10-02, by wenzelm
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
2008-10-02, by wenzelm
tuned
2008-10-02, by haftmann
Yet another proof of Newman's lemma, this time using the coherent logic prover.
2008-10-02, by berghofe
unit_source: more rigid parsing, stop after final qed;
2008-10-01, by wenzelm
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
2008-10-01, by wenzelm
replaced can_defer by is_relevant (negation);
2008-10-01, by wenzelm
datatype transition: internal trans field is maintained in reverse order;
2008-10-01, by wenzelm
future_proof: protect conclusion of deferred proof state;
2008-10-01, by wenzelm
future_schedule: back to one group for all loader tasks;
2008-10-01, by wenzelm
tuned comments;
2008-10-01, by wenzelm
fixed
2008-10-01, by haftmann
renamed promise to future, tuned related interfaces;
2008-10-01, by wenzelm
more robust treatment of Interrupt (cf. exn.ML);
2008-10-01, by wenzelm
more robust treatment of Interrupt;
2008-10-01, by wenzelm
more robust treatment of Interrupt (cf. exn.ML);
2008-10-01, by wenzelm
removed release_results (cf. Exn.release_all, Exn.release_first);
2008-10-01, by wenzelm
more precise join_futures, improved termination;
2008-10-01, by wenzelm
added more_antiquote.ML
2008-10-01, by haftmann
extract Isabelle dist name correctly
2008-10-01, by kleing
unit_source: explicit treatment of 'oops' proofs;
2008-09-30, by wenzelm
promise_proof: proper statement with empty vars;
2008-09-30, by wenzelm
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
2008-09-30, by wenzelm
schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
2008-09-30, by wenzelm
added unit_source: commands with proof;
2008-09-30, by wenzelm
begin_proof: avoid race condition wrt. skip_proofs flag;
2008-09-30, by wenzelm
load_thy: Toplevel.excursion based on units of command/proof pairs;
2008-09-30, by wenzelm
more command categories;
2008-09-30, by wenzelm
renamed Future.fork_irrelevant to Future.fork_background;
2008-09-30, by wenzelm
export explicit joint_futures, removed Theory.at_end hook;
2008-09-30, by wenzelm
tuned
2008-09-30, by haftmann
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
2008-09-30, by wenzelm
Toplevel.commit_exit: position;
2008-09-30, by wenzelm
export setmp_thread_position;
2008-09-30, by wenzelm
simplified process_file, eliminated Toplevel.excursion;
2008-09-30, by wenzelm
clarified codegen interfaces
2008-09-30, by haftmann
tuned
2008-09-30, by haftmann
reorganized examples
2008-09-30, by haftmann
fixed slips
2008-09-30, by haftmann
re-canibalised manual
2008-09-30, by haftmann
slightly different command line for makedist_mercurial
2008-09-30, by kleing
put_thms: ContextPosition.set_visible false;
2008-09-29, by wenzelm
added type pp, which helps installing polymorphic pretty printers;
2008-09-29, by wenzelm
added str_of;
2008-09-29, by wenzelm
install_pp Future.T (polyml only);
2008-09-29, by wenzelm
report_token/parse_token: back to context-less version;
2008-09-29, by wenzelm
back to plain Position.report for regular references;
2008-09-29, by wenzelm
back to plain Position.report for regular references;
2008-09-29, by wenzelm
promise global proofs;
2008-09-29, by wenzelm
renamed report to report_visible;
2008-09-29, by wenzelm
code example: back to individual ML commands, which are now thread-safe;
2008-09-29, by wenzelm
ContextPosition.report;
2008-09-29, by wenzelm
target update: invisible context position avoids duplication of reports etc.;
2008-09-29, by wenzelm
Context position visibility.
2008-09-29, by wenzelm
added context_position.ML;
2008-09-29, by wenzelm
more precise redundancy check
2008-09-29, by haftmann
clarified dependencies between arith tools
2008-09-29, by haftmann
separate HOL-Main image
2008-09-29, by haftmann
polished code generator setup
2008-09-29, by haftmann
added theory antiquotation
2008-09-29, by haftmann
tuned comments;
2008-09-29, by wenzelm
handle _ should be avoided (spurious Interrupt will spoil the game);
2008-09-29, by wenzelm
added norm_export_morphism;
2008-09-29, by wenzelm
added exit_global, exit_result, exit_result_global;
2008-09-29, by wenzelm
LocalTheory.exit_global;
2008-09-29, by wenzelm
HOL no longer depends on HOL-Plain;
2008-09-28, by wenzelm
setmp_noncritical;
2008-09-28, by wenzelm
join earlier promises first;
2008-09-28, by wenzelm
proper setmp_thread_data for nested execute (cf. join_loop);
2008-09-28, by wenzelm
promise_result: enforce strictly sequential dependencies, via serial numbers;
2008-09-28, by wenzelm
do not cvs update for doc test (switching to mercurial, update done outside
2008-09-28, by kleing
use mercurial repository for isatest
2008-09-28, by kleing
thread_data: include thread name, export access;
2008-09-28, by wenzelm
setmp_noncritical;
2008-09-27, by wenzelm
dequeue_towards: return bound for unfinished tasks;
2008-09-27, by wenzelm
moved release_results to future.ML;
2008-09-27, by wenzelm
added release_results (formerly in par_list.ML);
2008-09-27, by wenzelm
Future.release_results;
2008-09-27, by wenzelm
more tracing;
2008-09-27, by wenzelm
Theory.checkpoint for main operations, admits concurrent proofs;
2008-09-27, by wenzelm
promise: include check into future body, i.e. joined results are always valid;
2008-09-27, by wenzelm
proper transfer of theorems that involve classes being instantiated here;
2008-09-27, by wenzelm
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
2008-09-27, by wenzelm
eliminated polymorphic equality;
2008-09-26, by wenzelm
added subset operation;
2008-09-26, by wenzelm
Added fresh_star_const.
2008-09-26, by berghofe
Added some more theorems to NominalData.
2008-09-26, by berghofe
Added some more lemmas that are useful in proof of strong induction rule.
2008-09-26, by berghofe
removed obsolete name convention "func"
2008-09-26, by haftmann
fixed typo
2008-09-26, by haftmann
clarified function transformator interface
2008-09-26, by haftmann
op = vs. eq
2008-09-26, by haftmann
moved future_scheduler flag to skip_proof.ML;
2008-09-25, by wenzelm
added future_scheduler (from thy_info.ML);
2008-09-25, by wenzelm
simplified promise;
2008-09-25, by wenzelm
simplified Thm.promise;
2008-09-25, by wenzelm
explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove;
2008-09-25, by wenzelm
explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
2008-09-25, by wenzelm
circumvent problem with code redundancy
2008-09-25, by haftmann
clarifed redundancy policy
2008-09-25, by haftmann
tuned comments;
2008-09-25, by wenzelm
added release_results;
2008-09-25, by wenzelm
abtract types: plain datatype with opaque signature matching;
2008-09-25, by wenzelm
prove: error with original thread position;
2008-09-25, by wenzelm
explicit type OrdList.T;
2008-09-25, by wenzelm
(temporary workaround)
2008-09-25, by haftmann
(temporal deactivation)
2008-09-25, by haftmann
non left-linear equations for nbe
2008-09-25, by haftmann
non left-linear equations for nbe
2008-09-25, by haftmann
map_force
2008-09-25, by haftmann
matchess
2008-09-25, by haftmann
burrow_fst
2008-09-25, by haftmann
discontinued special treatment of op = vs. eq_class.eq
2008-09-25, by haftmann
report: produce individual status messages;
2008-09-24, by wenzelm
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
2008-09-24, by wenzelm
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
2008-09-24, by wenzelm
init: OuterKeyword.report;
2008-09-24, by wenzelm
prove_multi: immediate;
2008-09-23, by wenzelm
added promise_result, prove_promise;
2008-09-23, by wenzelm
Corrected call of SUBPROOF in coherent_tac that used wrong context.
2008-09-23, by berghofe
fixed outer syntax
2008-09-23, by haftmann
case default fallback for NBE
2008-09-23, by haftmann
fixed quickcheck parameter syntax
2008-09-23, by haftmann
renamed rtype to typerep
2008-09-23, by haftmann
added fold_rev;
2008-09-23, by wenzelm
added del_node, which is more efficient for sparse graphs;
2008-09-23, by wenzelm
IntGraph.del_node;
2008-09-23, by wenzelm
join_results: special case for empty list, works without multithreading;
2008-09-23, by wenzelm
added dest_deriv, removed external type deriv;
2008-09-23, by wenzelm
added conditional add_oracles, keep oracles_of_proof private;
2008-09-23, by wenzelm
Thm.proof_of;
2008-09-23, by wenzelm
Added coherent logic prover.
2008-09-22, by berghofe
New prover for coherent logic.
2008-09-22, by berghofe
Added setup for coherent logic prover.
2008-09-22, by berghofe
Added examples for coherent logic prover.
2008-09-22, by berghofe
Examples for coherent logic prover.
2008-09-22, by berghofe
made the perm_simp tactic to understand options such as (no_asm)
2008-09-22, by urbanc
type thm: fully internal derivation, no longer exported;
2008-09-22, by wenzelm
added is_finished;
2008-09-22, by wenzelm
added Promise constructor, which is similar to Oracle but may be replaced later;
2008-09-22, by wenzelm
removed deriv.ML which is now incorporated into thm.ML;
2008-09-22, by wenzelm
added reject_draft;
2008-09-22, by wenzelm
type thm: fully internal derivation, no longer exported;
2008-09-22, by wenzelm
generic quickcheck framework
2008-09-22, by haftmann
TEMPORARY: make batch run happy
2008-09-22, by haftmann
absolute Library path
2008-09-22, by haftmann
different session branches for HOL-Plain vs. Plain
2008-09-22, by haftmann
temporary workaround for class constants
2008-09-22, by haftmann
corrected sort intersection
2008-09-22, by haftmann
some steps towards generic quickcheck framework
2008-09-22, by haftmann
fixed headers
2008-09-22, by haftmann
added some fragments from website
2008-09-22, by haftmann
made SML/NJ happy;
2008-09-20, by wenzelm
Isar toplevel editor model.
2008-09-19, by wenzelm
future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-19, by wenzelm
output_sync is now public;
2008-09-19, by wenzelm
added props_text (from isar_syn.ML);
2008-09-19, by wenzelm
moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-19, by wenzelm
moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-19, by wenzelm
added Isar/isar.scala;
2008-09-19, by wenzelm
avoid using implicit assumptions
2008-09-19, by huffman
add theory graph to ZF document
2008-09-19, by huffman
made SMLNJ happy
2008-09-19, by haftmann
jar: include sources;
2008-09-18, by wenzelm
tuned;
2008-09-18, by wenzelm
eval_term: CRITICAL due to eval_result;
2008-09-18, by wenzelm
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
2008-09-18, by wenzelm
updated generated file;
2008-09-18, by wenzelm
simplified oracle interface;
2008-09-18, by wenzelm
show: non-critical testing;
2008-09-18, by wenzelm
added deriv.ML: Abstract derivations based on raw proof terms.
2008-09-18, by wenzelm
termination prover for "fun" can be configured using context data.
2008-09-18, by krauss
updated generated file;
2008-09-18, by wenzelm
unchecked $ISABELLE_HOME_USER/etc/settings;
2008-09-18, by wenzelm
use_text/use_file now depend on explicit ML name space;
2008-09-17, by wenzelm
threads work only for Poly/ML 5.2 or later;
2008-09-17, by wenzelm
* ML bindings produced via Isar commands are stored within the Isar context.
2008-09-17, by wenzelm
added ML_prf;
2008-09-17, by wenzelm
updated generated file;
2008-09-17, by wenzelm
added inherit_env;
2008-09-17, by wenzelm
added map_contexts;
2008-09-17, by wenzelm
ML_prf: inherit env for all contexts within the proof;
2008-09-17, by wenzelm
shutdown only if Multithreading.available;
2008-09-17, by wenzelm
ML_Context.evaluate: proper context (for ML environment);
2008-09-17, by wenzelm
ML_Context.evaluate: proper context (for ML environment);
2008-09-17, by wenzelm
simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-17, by wenzelm
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
2008-09-17, by wenzelm
simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-17, by wenzelm
explicit handling of ML environment within generic context;
2008-09-17, by wenzelm
added ML_prf;
2008-09-17, by wenzelm
use_text/use_file now depend on explicit ML name space;
2008-09-17, by wenzelm
ML name space -- dummy version of Poly/ML 5.2 facility.
2008-09-17, by wenzelm
added ML-Systems/ml_name_space.ML;
2008-09-17, by wenzelm
use ML_prf within proofs;
2008-09-17, by wenzelm
local @{context};
2008-09-17, by wenzelm
moved global ML bindings to global place;
2008-09-17, by wenzelm
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-17, by wenzelm
updated generated file;
2008-09-17, by wenzelm
wf_finite_psubset[simp], in_finite_psubset[simp]
2008-09-17, by krauss
Public interface to interpretation morphism.
2008-09-17, by ballarin
moved term_of syntax to separate theory
2008-09-17, by haftmann
removed obsolete theory
2008-09-17, by haftmann
added quickcheck.ML
2008-09-17, by haftmann
tuned comments;
2008-09-16, by wenzelm
multithreading for Poly/ML 5.1 is no longer supported;
2008-09-16, by wenzelm
tuned;
2008-09-16, by wenzelm
updated system manual;
2008-09-16, by wenzelm
Proof General / Emacs interface wrapper;
2008-09-16, by wenzelm
Proof General: option -I is obsolete;
2008-09-16, by wenzelm
added PROOFGENERAL_HOME;
2008-09-16, by wenzelm
separate emacs tool for Proof General / Emacs;
2008-09-16, by wenzelm
added quickcheck stub
2008-09-16, by haftmann
removed babel again
2008-09-16, by haftmann
celver code lemma avoid type ambiguity problem with Haskell
2008-09-16, by haftmann
a sophisticated char/nibble conversion combinator
2008-09-16, by haftmann
moved term_of syntax to separate theory
2008-09-16, by haftmann
SimpleThread.fork;
2008-09-16, by wenzelm
Simplified thread fork interface.
2008-09-16, by wenzelm
added Concurrent/simple_thread.ML;
2008-09-16, by wenzelm
updated generated file;
2008-09-16, by wenzelm
misc tuning and modernization;
2008-09-16, by wenzelm
check setting and tool;
2008-09-16, by wenzelm
Clearer separation of interpretation frontend and backend.
2008-09-16, by ballarin
No interpretation of locale with dangling type frees.
2008-09-16, by ballarin
Do not rely on locale assumption in interpretation.
2008-09-16, by ballarin
The metis method now fails in the usual manner, rather than raising an exception,
2008-09-16, by paulson
Fixed typo in locale declaration.
2008-09-16, by ballarin
added babel
2008-09-16, by haftmann
explicit size of characters
2008-09-16, by haftmann
dropped superfluous code lemmas
2008-09-16, by haftmann
evaluation using code generator
2008-09-16, by haftmann
generic value command
2008-09-16, by haftmann
converted symbols.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
converted misc.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
generated files;
2008-09-15, by wenzelm
converted present.tex;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
load underscore package after iman etc.;
2008-09-15, by wenzelm
tuned comment;
2008-09-15, by wenzelm
added formal markup for setting, executable, tool;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
converted basics.tex to theory file;
2008-09-15, by wenzelm
added isatt markup;
2008-09-15, by wenzelm
New outline for codegen tutorial -- draft
2008-09-14, by haftmann
added extern_fact (local or global);
2008-09-12, by wenzelm
print raw (internal) result names;
2008-09-12, by wenzelm
more procise printing of fact names;
2008-09-12, by wenzelm
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-12, by wenzelm
cancel, shutdown: notify_all;
2008-09-11, by wenzelm
finish: Future.shutdown last;
2008-09-11, by wenzelm
eliminated requests, use global state variables uniformly;
2008-09-11, by wenzelm
finish: Future.shutdown;
2008-09-11, by wenzelm
added is_empty;
2008-09-11, by wenzelm
shutdown: global join-and-shutdown operation;
2008-09-11, by wenzelm
added focus, which indicates a particular collection of high-priority tasks;
2008-09-11, by wenzelm
some general notes on future values;
2008-09-11, by wenzelm
separate Concurrent/ROOT.ML;
2008-09-11, by wenzelm
Parallel list combinators.
2008-09-11, by wenzelm
added Concurrent/par_list.ML;
2008-09-11, by wenzelm
added interrupt_task (external id);
2008-09-10, by wenzelm
tuned;
2008-09-10, by wenzelm
future_schedule: uninterruptible join;
2008-09-10, by wenzelm
added future_scheduler (default false);
2008-09-10, by wenzelm
replaced join_all by join_results, which returns Exn.results;
2008-09-10, by wenzelm
workers: explicit activity flag;
2008-09-10, by wenzelm
future: allow explicit group;
2008-09-10, by wenzelm
cancel: invalidate group implicitly, via bool ref;
2008-09-10, by wenzelm
auto_flush: uniform block buffering for all output streams;
2008-09-10, by wenzelm
auto_flush stdout, stderr as well;
2008-09-09, by wenzelm
proper values of no_interrupts, regular_interrupts;
2008-09-09, by wenzelm
cancel: check_scheduler;
2008-09-09, by wenzelm
simplified dequeue: provide Thread.self internally;
2008-09-09, by wenzelm
eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09, by wenzelm
export get_first from underlying table;
2008-09-09, by wenzelm
out_stream: block-buffered, with separate autoflush thread (every 50ms);
2008-09-09, by wenzelm
babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
2008-09-09, by wenzelm
added comment
2008-09-09, by nipkow
human-readable printing of TaskQueue.task/group;
2008-09-09, by wenzelm
* Changed defaults for unify configuration options;
2008-09-09, by wenzelm
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
2008-09-09, by wenzelm
job: explicit 'ok' status -- false for canceled jobs;
2008-09-09, by wenzelm
Overall exception handler in order to insulate our users from low-level bugs.
2008-09-09, by paulson
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-09-09, by paulson
Increasing the default limits in order to prevent unnecessary failures.
2008-09-09, by paulson
send: broadcast condition while locked!
2008-09-08, by wenzelm
proper signature constraint;
2008-09-08, by wenzelm
tuned Mailbox.send;
2008-09-08, by wenzelm
removed unused sync_interrupts;
2008-09-08, by wenzelm
moved thread data to future.ML (again);
2008-09-08, by wenzelm
more interrupt operations;
2008-09-08, by wenzelm
moved task, thread_data, group, queue to task_queue.ML;
2008-09-08, by wenzelm
Ordered queue of grouped tasks.
2008-09-08, by wenzelm
added Concurrent/task_queue.ML;
2008-09-08, by wenzelm
await: SYNCHRONIZED wait!
2008-09-08, by wenzelm
tuned check_cache;
2008-09-08, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
opaque signature constraint abstracts local type abbrev;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
added change_result;
2008-09-07, by wenzelm
Functional threads as future values.
2008-09-07, by wenzelm
added Concurrent/future.ML;
2008-09-07, by wenzelm
Default (mostly dummy) implementation of thread structures.
2008-09-07, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2008-09-07, by wenzelm
*** empty log message ***
2008-09-07, by wenzelm
explicit use of universal.ML and dummy_thread.ML;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
send: broadcast to all waiting threads;
2008-09-07, by wenzelm
added ML-Systems/thread_dummy.ML;
2008-09-07, by wenzelm
dropped "run" marker in monad syntax
2008-09-06, by haftmann
multithreading.ML provides dummy thread structures;
2008-09-05, by wenzelm
different bookkeeping for code equations
2008-09-05, by haftmann
renamed structure CodeTarget to Code_Target
2008-09-05, by haftmann
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
2008-09-05, by huffman
proper header;
2008-09-04, by wenzelm
added receive_timeout;
2008-09-04, by wenzelm
check WRAPPER_OUTPUT node type;
2008-09-04, by wenzelm
init: disallow "" as out stream;
2008-09-04, by wenzelm
fixed deps: no Concurrent/receiver.ML yet;
2008-09-04, by wenzelm
Concurrent message exchange via mailbox -- with unbounded queueing.
2008-09-04, by wenzelm
added Concurrent/mailbox.ML;
2008-09-04, by wenzelm
reorganize subsections
2008-09-04, by huffman
rename INF_drop_prefix to INFM_drop_prefix
2008-09-04, by huffman
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
2008-09-04, by huffman
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
2008-09-04, by huffman
tuned signature;
2008-09-04, by wenzelm
added General/queue.ML;
2008-09-04, by wenzelm
Efficient queues.
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML
2008-09-04, by wenzelm
multithreading.ML provides dummy thread structures;
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML;
2008-09-04, by wenzelm
provide dummy thread structures, including proper Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Scheduling -- multiple threads working on a queue of tasks.
2008-09-04, by wenzelm
added Concurrent/schedule.ML;
2008-09-04, by wenzelm
update tags
2008-09-03, by convert-repo
use /home/isabelle/mercurial/bin/hg wrapper;
2008-09-03, by wenzelm
exclude large .mov files;
2008-09-03, by wenzelm
simplified add_axiom: no hyps;
2008-09-03, by wenzelm
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-03, by wenzelm
axiomatization is now global-only;
2008-09-03, by wenzelm
added const_decl;
2008-09-03, by wenzelm
simplified specify_const: canonical args, global deps;
2008-09-03, by wenzelm
declare_const: Name.binding, store/report position;
2008-09-03, by wenzelm
Sign.declare_const: Name.binding;
2008-09-03, by wenzelm
removed ex/Puzzle
2008-09-03, by nipkow
added qualified: string -> binding -> binding;
2008-09-03, by wenzelm
Name.qualified;
2008-09-03, by wenzelm
theorem dependency hook: check previous state;
2008-09-03, by wenzelm
added pos_of;
2008-09-03, by wenzelm
-> AFP
2008-09-03, by nipkow
simplified Toplevel.add_hook: cover successful transactions only;
2008-09-03, by wenzelm
retired Ben Porter's DenumRat in favour of the shorter proof in
2008-09-03, by kleing
made SML/NJ happy;
2008-09-02, by wenzelm
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
2008-09-02, by wenzelm
* Generic Toplevel.add_hook interface allows to analyze the result of
2008-09-02, by wenzelm
Replaced Library/NatPair by Nat_Int_Bij.
2008-09-02, by nipkow
added new_thms_deps (operates on global facts, some name_hint approximation);
2008-09-02, by wenzelm
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
2008-09-02, by wenzelm
added add_hook interface for post-transition hooks;
2008-09-02, by wenzelm
tuned;
2008-09-02, by wenzelm
ProofDisplay.print_results;
2008-09-02, by wenzelm
no pervasive bindings;
2008-09-02, by wenzelm
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
2008-09-02, by nipkow
distributed literal code generation out of central infrastructure
2008-09-02, by haftmann
* Result facts now refer to the *full* internal name;
2008-09-02, by wenzelm
* Name bindings in higher specification mechanisms;
2008-09-02, by wenzelm
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-09-02, by wenzelm
updated generated file;
2008-09-02, by wenzelm
Interpretation commands no longer accept interpretation attributes.
2008-09-02, by ballarin
type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
added binding;
2008-09-02, by wenzelm
added fixed_decl, fact_decl, local_fact_decl;
2008-09-02, by wenzelm
name_thm etc.: pass position;
2008-09-02, by wenzelm
added type binding -- generic name bindings;
2008-09-02, by wenzelm
name/var morphism operates on Name.binding;
2008-09-02, by wenzelm
adapted to class instantiation compliance
2008-09-02, by haftmann
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
2008-09-01, by nipkow
renamed lemma
2008-09-01, by nipkow
moved more lemmas here from AFP/Integration/Rats
2008-09-01, by nipkow
moved lemma into SetInterval where it belongs
2008-09-01, by nipkow
cleaned up code generation for {.._} and {..<_}
2008-09-01, by nipkow
*** empty log message ***
2008-09-01, by nipkow
extended interface to preferences to allow adding new ones
2008-09-01, by nipkow
Prover is set via menu now
2008-09-01, by nipkow
restructured code generation of literals
2008-09-01, by haftmann
IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
2008-08-29, by wenzelm
init: more explicit protocol of open/remove rendezvous;
2008-08-29, by wenzelm
use hardwired /tmp -- fifo only work on local file-system;
2008-08-29, by wenzelm
separate module for code output
2008-08-29, by haftmann
fixed names of class assumptions
2008-08-29, by haftmann
dropped parameter prefix for class theorems
2008-08-29, by haftmann
added charset (from isabelle_process.scala);
2008-08-28, by wenzelm
moved charset to isabelle_system.scala;
2008-08-28, by wenzelm
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
2008-08-28, by wenzelm
restructured and split code serializer module
2008-08-28, by haftmann
no parameter prefix for class interpretation
2008-08-28, by haftmann
updated
2008-08-28, by haftmann
tuned fold_lines;
2008-08-28, by wenzelm
fold_lines: simplified, more efficient due to String.fields;
2008-08-28, by wenzelm
rm fifo after open;
2008-08-28, by wenzelm
dummy setup for completion;
2008-08-28, by wenzelm
create named pipe;
2008-08-28, by wenzelm
added is_cygwin;
2008-08-28, by wenzelm
join stdout/stderr, eliminated Kind.STDERR;
2008-08-28, by wenzelm
explicit output stream, typically a named pipe;
2008-08-28, by wenzelm
refined option -W: output stream;
2008-08-28, by wenzelm
more function -> fun
2008-08-28, by krauss
quicksort: function -> fun
2008-08-28, by krauss
corrected some typos
2008-08-28, by krauss
fixed atom_to_xml: literal "name" attribute;
2008-08-28, by wenzelm
exported atom_to_xml;
2008-08-28, by wenzelm
changed Markup print mode to YXML -- explicitly decode messages before being issued;
2008-08-28, by wenzelm
tuned;
2008-08-28, by wenzelm
present_token: disable print_mode, which is YXML now;
2008-08-28, by wenzelm
text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;
2008-08-28, by wenzelm
removed obsolete XML.Output workaround;
2008-08-28, by wenzelm
added get_int;
2008-08-28, by wenzelm
removed obsolete get_string;
2008-08-28, by wenzelm
removed obsolete ProofGeneral/pgml_isabelle.ML;
2008-08-28, by wenzelm
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
2008-08-27, by huffman
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
load buffer.ML before file.ML;
2008-08-27, by wenzelm
replaced find_substring by first_field;
2008-08-27, by wenzelm
Consistent naming of theorems in interpretation.
2008-08-27, by ballarin
simplified parse_attrib (find_substring instead of space_explode);
2008-08-27, by wenzelm
added find_substring;
2008-08-27, by wenzelm
added HOL/ex/Numeral.thy
2008-08-27, by haftmann
get rid of tabs;
2008-08-27, by wenzelm
Property lists.
2008-08-27, by wenzelm
added General/properties.ML;
2008-08-27, by wenzelm
type Properties.T;
2008-08-27, by wenzelm
proper error message
2008-08-27, by haftmann
proper handling of type variabl names
2008-08-27, by haftmann
completing arities after subclass instance
2008-08-27, by haftmann
untabification
2008-08-27, by haftmann
tuned code generator setup
2008-08-27, by haftmann
added equivariance lemmas for ex1 and the
2008-08-27, by urbanc
add lemmas about Rats similar to those about Reals
2008-08-27, by huffman
move real_vector class proofs into vector_space and group_hom locales
2008-08-26, by huffman
added distributivity of relation composition over union [simp]
2008-08-26, by krauss
tuned append;
2008-08-26, by wenzelm
command: symbols.encode;
2008-08-26, by wenzelm
Reorganisation of registration code.
2008-08-26, by ballarin
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
2008-08-26, by krauss
purge classes after compilation;
2008-08-26, by wenzelm
renamed Isabelle-repository to isabelle;
2008-08-26, by wenzelm
Defined rationals (Rats) globally in Rational.
2008-08-26, by nipkow
replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;
2008-08-26, by wenzelm
moved new Symbol.Interpretation into plugin;
2008-08-25, by wenzelm
promoted to EBPlugin;
2008-08-25, by wenzelm
explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;
2008-08-25, by wenzelm
tuned;
2008-08-25, by wenzelm
isabelle process: pick options/args from properties;
2008-08-25, by wenzelm
removed unused ConsolePlugin dependency;
2008-08-25, by wenzelm
simplified exceptions: use plain error function / RuntimeException;
2008-08-25, by wenzelm
added try_result;
2008-08-25, by wenzelm
misc reorganization;
2008-08-24, by wenzelm
Kind: added is_control;
2008-08-24, by wenzelm
get: allow null;
2008-08-24, by wenzelm
misc tuning of names;
2008-08-24, by wenzelm
rearranged source files;
2008-08-24, by wenzelm
init_message: class markup in message body, not header;
2008-08-24, by wenzelm
repackaged as isabelle.jedit;
2008-08-24, by wenzelm
untabify: silently turn tab into space if column information is unavailable;
2008-08-24, by wenzelm
corrected cache handling for class operations
2008-08-24, by haftmann
default replaces arbitrary
2008-08-24, by haftmann
tuned import order
2008-08-24, by haftmann
activated \<A>, \<a>, \<AA>, \<aa>;
2008-08-24, by wenzelm
* Isabelle/lib/classes/Pure.jar;
2008-08-23, by wenzelm
jars: removed obsolete Java process wrapper (cf. new Pure.jar);
2008-08-23, by wenzelm
obsolete;
2008-08-23, by wenzelm
obsolete -- superceded by Pure.jar (Scala version);
2008-08-23, by wenzelm
updated to Pure.jar;
2008-08-23, by wenzelm
added exec;
2008-08-23, by wenzelm
moved class Result into static object, removed dynamic tree method;
2008-08-23, by wenzelm
symbolic message markup;
2008-08-23, by wenzelm
renamed Markup.MALFORMED to Markup.BAD;
2008-08-23, by wenzelm
added position, messages;
2008-08-23, by wenzelm
added messages and process information;
2008-08-23, by wenzelm
Position properties.
2008-08-23, by wenzelm
added General/position.scala;
2008-08-23, by wenzelm
adapted to new IsabelleProcess from Pure.jar;
2008-08-23, by wenzelm
include ../../classes/Pure.jar;
2008-08-23, by wenzelm
added const Rational
2008-08-23, by nipkow
YXML.parse_failsafe;
2008-08-23, by wenzelm
shell_prefix: physical /bin/env on Cygwin;
2008-08-23, by wenzelm
removed full_markup mode (default);
2008-08-23, by wenzelm
added parse_failsafe;
2008-08-23, by wenzelm
refer to symbolic Markup;
2008-08-23, by wenzelm
Common markup elements.
2008-08-23, by wenzelm
added General/markup.scala;
2008-08-23, by wenzelm
BadVariable: toString;
2008-08-23, by wenzelm
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
2008-08-23, by wenzelm
append_string: proper backslash in character escapes;
2008-08-23, by wenzelm
added getenv;
2008-08-23, by wenzelm
tuned;
2008-08-23, by wenzelm
Isabelle outer syntax.
2008-08-23, by wenzelm
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
2008-08-23, by wenzelm
Isabelle process management -- always reactive due to multi-threaded I/O.
2008-08-23, by wenzelm
renamed DOM to document, add xml version and optional stylesheets;
2008-08-23, by wenzelm
tuned comments;
2008-08-22, by wenzelm
parse_attrib: proper index of name end!
2008-08-21, by wenzelm
tuned parse performance: avoid splitting terminal Y chunk;
2008-08-21, by wenzelm
parse_attrib: more efficient due to indexOf('=');
2008-08-21, by wenzelm
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
2008-08-21, by wenzelm
tuned comment;
2008-08-21, by wenzelm
added iterator over content;
2008-08-21, by wenzelm
proper ISABELLE_ROOT_JVM on Cygwin;
2008-08-21, by wenzelm
pattern: proper "." not "[.]"!
2008-08-21, by wenzelm
recode: proper result for unmatched symbols;
2008-08-21, by wenzelm
more robust pattern: look at longer matches first, added catch-all case;
2008-08-21, by wenzelm
added get_setting;
2008-08-21, by wenzelm
read_symbols: proper IsabelleSystem.platform_path;
2008-08-21, by wenzelm
added ISABELLE_ROOT_JVM;
2008-08-21, by wenzelm
Theorem on polynomial division and lemmas.
2008-08-18, by ballarin
removed parse_element -- no longer fits to liberal parse!
2008-08-17, by wenzelm
Minimalistic XML tree values.
2008-08-17, by wenzelm
Efficient text representation of XML trees.
2008-08-17, by wenzelm
added General/xml.scala, General/yxml.scala;
2008-08-17, by wenzelm
decode escaped symbols as well;
2008-08-17, by wenzelm
tuned Recoder;
2008-08-16, by wenzelm
more private fields;
2008-08-16, by wenzelm
jar: invoke scaladoc;
2008-08-16, by wenzelm
tuned comments;
2008-08-16, by wenzelm
use scala.collection.jcl.HashMap, which seems to be more efficient;
2008-08-16, by wenzelm
jar target: removed jvmpath -- does not work on Linux!?
2008-08-16, by wenzelm
add scala-library.jar if available;
2008-08-16, by wenzelm
jar target: jvmpath;
2008-08-16, by wenzelm
Isabelle system support.
2008-08-16, by wenzelm
reading symbol interpretation tables;
2008-08-16, by wenzelm
added Tools/isabelle_system.scala;
2008-08-16, by wenzelm
removed unused usage;
2008-08-16, by wenzelm
more robust handling of directory layout variants;
2008-08-16, by wenzelm
refined scala/java wrappers via isatool;
2008-08-16, by wenzelm
tuned abbrevs;
2008-08-16, by wenzelm
added ISABELLE_SCALA, ISABELLE_JAVA;
2008-08-16, by wenzelm
added ISABELLE_HOME_JVM;
2008-08-15, by wenzelm
proper jvmpath for cygwin;
2008-08-15, by wenzelm
proper RC;
2008-08-15, by wenzelm
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
2008-08-15, by wenzelm
refined JVM path wrappers;
2008-08-15, by wenzelm
added JVM components (Scala or Java);
2008-08-15, by wenzelm
tuned;
2008-08-15, by wenzelm
jars: build Pure.jar;
2008-08-15, by wenzelm
scan: proper recovery for escaped \\< symbols;
2008-08-15, by wenzelm
basic setup for Scala material;
2008-08-15, by wenzelm
Basic support for Isabelle symbols.
2008-08-15, by wenzelm
added some abbrevs;
2008-08-15, by wenzelm
removed redundant "symbol" property;
2008-08-15, by wenzelm
Default interpretation of some Isabelle symbols.
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
fixed DOCTYPE -- XHTML is case-sensitive!
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
added ML_antiq, doc_antiq;
2008-08-15, by wenzelm
added README;
2008-08-15, by wenzelm
generated truetype font;
2008-08-15, by wenzelm
The Jerusalem font from 2004 -- unicode version.
2008-08-15, by wenzelm
args: explicit groups for file_name, theory_name;
2008-08-15, by wenzelm
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
2008-08-15, by wenzelm
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
2008-08-15, by wenzelm
token_kind: add Space, Comment;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
output_markup: check Markup.is_none;
2008-08-15, by wenzelm
added is_none;
2008-08-15, by wenzelm
Args.name_source(_position) for proper position information;
2008-08-15, by wenzelm
[source=false] for quoted antiquotation avoids quote-escapes in output;
2008-08-14, by wenzelm
report antiquotations;
2008-08-14, by wenzelm
tuned;
2008-08-14, by wenzelm
report ML_source;
2008-08-14, by wenzelm
renamed P.ml_source to P.ML_source;
2008-08-14, by wenzelm
report doc_source;
2008-08-14, by wenzelm
added ML_source, doc_source;
2008-08-14, by wenzelm
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-14, by wenzelm
added source_of';
2008-08-14, by wenzelm
P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-14, by wenzelm
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-14, by wenzelm
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
retrieve_thms: transfer fact position to result;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-14, by wenzelm
made SML/NJ happy;
2008-08-14, by wenzelm
removed obsolete present_html -- now part of regular theory presentation;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
ProofDisplay.add_hook;
2008-08-13, by wenzelm
simplified present_local_theory/proof;
2008-08-13, by wenzelm
ProofDisplay.theory_results;
2008-08-13, by wenzelm
removed obsolete present_results;
2008-08-13, by wenzelm
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
2008-08-13, by wenzelm
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
2008-08-13, by wenzelm
simplified markup commands;
2008-08-13, by wenzelm
simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-13, by wenzelm
added untabify_content;
2008-08-13, by wenzelm
tuned;
2008-08-13, by wenzelm
removed obsolete untabify (superceded by SymbolPos.tabify_content);
2008-08-13, by wenzelm
tuned document;
2008-08-13, by wenzelm
removed obsolete theorems;
2008-08-13, by wenzelm
Changed proof of strong induction rule to avoid infinite loop
2008-08-13, by berghofe
token_kind_markup: complete coverage;
2008-08-12, by wenzelm
OuterSyntax.scan: pass position;
2008-08-12, by wenzelm
message: ignored if body empty;
2008-08-12, by wenzelm
load_thy: removed obsolete dir argument;
2008-08-12, by wenzelm
abstract type span, tuned interfaces;
2008-08-12, by wenzelm
adapted ThyEdit operations;
2008-08-12, by wenzelm
added ignored, malformed transitions;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
Isabelle.command: inline former OuterSyntax.prepare_command;
2008-08-12, by wenzelm
load thy_edit.ML before outer_syntax.ML;
2008-08-12, by wenzelm
renamed unknown_span to malformed_span;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
updated generated file;
2008-08-12, by wenzelm
rudimentary code setup for set operations
2008-08-11, by haftmann
<applet>: more XHTML 1.0 Transitional conformance;
2008-08-11, by wenzelm
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-11, by wenzelm
<pre>: removed xml:space, is already default;
2008-08-11, by wenzelm
produce XHTML 1.0 Transitional;
2008-08-11, by wenzelm
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-08-11, by wenzelm
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
2008-08-11, by wenzelm
changed code setup
2008-08-11, by haftmann
re-arranged class dense_linear_order
2008-08-11, by haftmann
rudimentary code setup for set operations
2008-08-11, by haftmann
moved class wellorder to theory Orderings
2008-08-11, by haftmann
added parse_token (from proof_context.ML);
2008-08-10, by wenzelm
read_tyname/const/const_proper: report position;
2008-08-10, by wenzelm
pass position to get_fact;
2008-08-10, by wenzelm
pass token source to typ/term etc.;
2008-08-10, by wenzelm
added name property operation;
2008-08-10, by wenzelm
renamed ML_Lex.val_of to content_of;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
load args.ML later (after outer_parse.ML);
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
read_asts: report literal tokens;
2008-08-09, by wenzelm
tuned error message;
2008-08-09, by wenzelm
pos_of_token: Position.T;
2008-08-09, by wenzelm
dest: sort strings;
2008-08-09, by wenzelm
added literal;
2008-08-09, by wenzelm
read_token: more robust handling of empty text;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
tuned SymbolPos interface;
2008-08-09, by wenzelm
YXML.parse: allow text without markup, potentially empty;
2008-08-09, by wenzelm
added content;
2008-08-09, by wenzelm
added distance_of (permissive version);
2008-08-09, by wenzelm
count offset as well;
2008-08-08, by wenzelm
added offset/end_offset;
2008-08-08, by wenzelm
tuned formatting;
2008-08-08, by wenzelm
clean up dead code
2008-08-08, by krauss
made SML/NJ happy;
2008-08-08, by wenzelm
FundefLib.try_proof : attempt a proof and see if it works
2008-08-08, by krauss
added lemmas
2008-08-08, by nipkow
inner_syntax markup is back;
2008-08-07, by wenzelm
disabled inner_syntax markup for now;
2008-08-07, by wenzelm
added read_token -- with optional YXML encoding of position;
2008-08-07, by wenzelm
parse_token: use Syntax.read_token, pass full position information;
2008-08-07, by wenzelm
tuned;
2008-08-07, by wenzelm
map_default: more explicit scope;
2008-08-07, by wenzelm
datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07, by wenzelm
simplified Antiquote signature;
2008-08-07, by wenzelm
more precise positions due to SymbolsPos.implode_delim;
2008-08-07, by wenzelm
simplified Antiq: regular SymbolPos.text with position;
2008-08-07, by wenzelm
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
2008-08-07, by wenzelm
only increment column if valid;
2008-08-07, by wenzelm
install_pp Position.T;
2008-08-07, by wenzelm
Position.start;
2008-08-07, by wenzelm
SymbolPos.explode;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
Antiquote.read/read_arguments;
2008-08-07, by wenzelm
updated type of nested sources;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
adapted Scan.extend_lexicon/merge_lexicons;
2008-08-07, by wenzelm
renamed scan_antiquotes to read;
2008-08-07, by wenzelm
export not_eof;
2008-08-07, by wenzelm
reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-07, by wenzelm
advance: single argument (again);
2008-08-07, by wenzelm
Symbols with explicit position information.
2008-08-07, by wenzelm
added General/symbol_pos.ML;
2008-08-07, by wenzelm
Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-06, by ballarin
added lemma
2008-08-06, by nipkow
made SML/NJ happy;
2008-08-06, by wenzelm
Reverted last change, since it caused incompatibilities.
2008-08-06, by berghofe
fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
2008-08-06, by wenzelm
T.end_position_of;
2008-08-06, by wenzelm
adapted Antiq;
2008-08-06, by wenzelm
parse_sort/typ/term/prop: report markup;
2008-08-06, by wenzelm
sort/typ/term/prop: inner_syntax markup encodes original source position;
2008-08-06, by wenzelm
removed obsolete range_of (already included in position);
2008-08-06, by wenzelm
report markup;
2008-08-06, by wenzelm
Antiq: inner vs. outer position;
2008-08-06, by wenzelm
of_properties: observe Markup.position_properties';
2008-08-06, by wenzelm
added position_properties';
2008-08-06, by wenzelm
token: maintain of source, which retains original position information;
2008-08-05, by wenzelm
moved OuterLex.count here;
2008-08-05, by wenzelm
improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-05, by wenzelm
advance: operate on symbol list (less overhead);
2008-08-05, by wenzelm
added token;
2008-08-05, by wenzelm
fix HOL/ex/LexOrds.thy; add to regression
2008-08-05, by krauss
added report;
2008-08-05, by wenzelm
removed axiom;
2008-08-05, by wenzelm
get_fact: report position;
2008-08-05, by wenzelm
Facts.lookup: return static/dynamic status;
2008-08-05, by wenzelm
position scanner: encode token range;
2008-08-04, by wenzelm
added encode_range;
2008-08-04, by wenzelm
added end_line, end_column properties;
2008-08-04, by wenzelm
meta_subst: xsymbols make it work with clean Pure;
2008-08-04, by wenzelm
abstract type Scan.stopper, position taken from last input token;
2008-08-04, by wenzelm
abstract type Scan.stopper;
2008-08-04, by wenzelm
abstract type stopper, may depend on final input;
2008-08-04, by wenzelm
removed obsolete apply_theorems(_i);
2008-08-04, by wenzelm
tuned signature;
2008-08-04, by wenzelm
removed obsolete note_thms_cmd;
2008-08-04, by wenzelm
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
2008-08-04, by wenzelm
tuned description;
2008-08-04, by wenzelm
replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
2008-08-04, by wenzelm
Quoted terms in consts_code declarations are now preprocessed as well.
2008-08-04, by berghofe
Exported eval_wrapper.
2008-08-04, by berghofe
- corrected bogus comment for function inst_conj_all
2008-08-04, by berghofe
removed dead code
2008-08-04, by krauss
simplified prepare_command;
2008-08-04, by wenzelm
Isar.command: explicitly set transaction position, as required for prepare_command errors;
2008-08-04, by wenzelm
Updated locale tests.
2008-08-04, by ballarin
Generalised polynomial lemmas from cring to ring.
2008-08-01, by ballarin
Removed import and lparams from locale record.
2008-08-01, by ballarin
made setsum executable on int.
2008-08-01, by nipkow
Tuned (for the sake of a meaningless log entry).
2008-07-31, by ballarin
New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-30, by ballarin
added hint about writing "x : set xs".
2008-07-30, by nipkow
simple lifters
2008-07-30, by haftmann
dropped imperative monad bind
2008-07-30, by haftmann
facts_of
2008-07-30, by haftmann
improved morphism
2008-07-30, by haftmann
SML_imp, OCaml_imp
2008-07-30, by haftmann
clarified
2008-07-30, by haftmann
tuned
2008-07-30, by haftmann
Zorn's Lemma for partial orders.
2008-07-29, by ballarin
Definitions and some lemmas for reflexive orderings.
2008-07-29, by ballarin
Lemmas added
2008-07-29, by ballarin
New theory on divisibility.
2008-07-29, by ballarin
Renamed theorems;
2008-07-29, by ballarin
New theorems on summation.
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp].
2008-07-29, by ballarin
New theory on divisibility;
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp];
2008-07-29, by ballarin
Haskell now living in the RealWorld
2008-07-29, by haftmann
corrected Pure dependency
2008-07-29, by haftmann
added removeAll
2008-07-29, by nipkow
tuned; explicit export of element accessors
2008-07-29, by haftmann
PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-29, by haftmann
some steps towards explicit class target for canonical interpretation
2008-07-29, by haftmann
declare
2008-07-29, by haftmann
*** empty log message ***
2008-07-28, by nipkow
simplified a proof
2008-07-27, by urbanc
tuned function name
2008-07-26, by haftmann
tuned bootstrap order
2008-07-26, by haftmann
subclass now also works for subclasses with empty specificaton
2008-07-25, by haftmann
dropped PureThy.note; added PureThy.add_thm
2008-07-25, by haftmann
added class preorder
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
added explicit root theory; some tuning
2008-07-25, by haftmann
tuned
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
added explicit purge_data
2008-07-21, by haftmann
added code generation
2008-07-21, by haftmann
fixed code generator setup
2008-07-21, by haftmann
(adjusted)
2008-07-21, by haftmann
Tuned and corrected ideal_tac for algebra.
2008-07-21, by chaieb
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
2008-07-21, by chaieb
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
2008-07-21, by chaieb
Tuned and simplified proofs
2008-07-21, by chaieb
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
2008-07-21, by chaieb
Relevant rules added to algebra's context
2008-07-21, by chaieb
renamed item to span, renamed contructors;
2008-07-20, by wenzelm
adapted ThyEdit.span;
2008-07-20, by wenzelm
maintain token range;
2008-07-20, by wenzelm
tty loop: do not report status;
2008-07-20, by wenzelm
added type range;
2008-07-20, by wenzelm
renamed command span markup;
2008-07-20, by wenzelm
SideKickParsedData: minimal content;
2008-07-20, by wenzelm
(adjusted)
2008-07-20, by haftmann
(adjusted)
2008-07-20, by haftmann
added verification framework for the HeapMonad and quicksort as example for this framework
2008-07-19, by bulwahn
build jedit plugin only if jedit is available;
2008-07-19, by wenzelm
misc tuning;
2008-07-18, by wenzelm
more class instantiations
2008-07-18, by haftmann
refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-18, by haftmann
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-18, by haftmann
fixed Scala path;
2008-07-18, by wenzelm
tuned build order;
2008-07-17, by wenzelm
proper purge_tmp;
2008-07-17, by wenzelm
tuned message;
2008-07-17, by wenzelm
tuned line breaks (NB: generated text is inserted here);
2008-07-17, by wenzelm
proper usage message;
2008-07-17, by wenzelm
make Isabelle source distribution (via Mercurial);
2008-07-17, by wenzelm
explicit Distribution.changelog;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
ThyInfo.remove_thy;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
use ../isabelle.sty and ../isabellesym.sty;
2008-07-17, by wenzelm
tuned whitespace;
2008-07-17, by wenzelm
removed old checklist;
2008-07-17, by wenzelm
obsolete;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
discontinued maketags;
2008-07-17, by wenzelm
assume GNU tar and find;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
use ../isabellesym.sty, which is always available;
2008-07-17, by wenzelm
Admin/build browser;
2008-07-17, by wenzelm
less verbosity;
2008-07-17, by wenzelm
Administrative build -- finish Isabelle source distribution.
2008-07-17, by wenzelm
simplified proofs
2008-07-17, by krauss
beautified proofs
2008-07-17, by nipkow
added lemmas
2008-07-17, by nipkow
Added Standardization theory to nominal examples.
2008-07-16, by berghofe
Added Standardization theory.
2008-07-16, by berghofe
editor model: run interactively for now;
2008-07-16, by wenzelm
updated generated file;
2008-07-16, by wenzelm
identify: more informative id in Toplevel.debug mode;
2008-07-16, by wenzelm
shortlogentry/filelogentry: show shortdate and full description;
2008-07-16, by wenzelm
Removed uses of context element includes.
2008-07-16, by ballarin
added Isar.command, Isar.insert, Isar.remove (editor model);
2008-07-16, by wenzelm
export type id with no_id and create_command;
2008-07-16, by wenzelm
tuned;
2008-07-15, by wenzelm
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-15, by wenzelm
load thy_edit.ML before isar.ML;
2008-07-15, by wenzelm
modernized specifications and proofs;
2008-07-15, by wenzelm
Removed uses of context element includes.
2008-07-15, by ballarin
tuned
2008-07-15, by haftmann
tuned code theorem bookkeeping
2008-07-15, by haftmann
tuned changelogentry;
2008-07-15, by wenzelm
refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
2008-07-15, by wenzelm
support for command status;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
tuned;
2008-07-15, by wenzelm
simplified commit_exit;
2008-07-15, by wenzelm
simplified commit_exit: operate on previous node of final state, include warning here;
2008-07-15, by wenzelm
removed obsolete commit_exit;
2008-07-15, by wenzelm
added command 'linear_undo';
2008-07-15, by wenzelm
removed command 'redo';
2008-07-15, by wenzelm
adapted ThyInfo.end_theory;
2008-07-15, by wenzelm
dropped map; fixed swap
2008-07-15, by haftmann
curried gcd
2008-07-15, by haftmann
cover macbroy as well;
2008-07-14, by wenzelm
tuned filelogentry;
2008-07-14, by wenzelm
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
2008-07-14, by wenzelm
tuned message;
2008-07-14, by wenzelm
updated generated file;
2008-07-14, by wenzelm
inform_file_processed: Isar.init_point last!
2008-07-14, by wenzelm
removed HOL-Complex, which has been discontinued after Isabelle2008;
2008-07-14, by wenzelm
added HOL-Nominal image;
2008-07-14, by wenzelm
removed obsolete Pure/General/history.ML;
2008-07-14, by wenzelm
inform_file_processed: try harder not to fail, ensure
2008-07-14, by wenzelm
commit_exit: proper error;
2008-07-14, by wenzelm
export EXCURSION_FAIL;
2008-07-14, by wenzelm
dropped junk
2008-07-14, by haftmann
moved bootstrap of simplifier
2008-07-14, by haftmann
tuned
2008-07-14, by haftmann
end_theory: no result;
2008-07-14, by wenzelm
removed obsolete Toplevel.RESTART;
2008-07-14, by wenzelm
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
adapted IsarCmd.init_theory;
2008-07-14, by wenzelm
renamed theory to init_theory, removed obsolete kill argument;
2008-07-14, by wenzelm
added commit_exit;
2008-07-14, by wenzelm
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-07-14, by krauss
renamed conversions to _conv, tuned
2008-07-14, by krauss
Simplified proofs
2008-07-14, by chaieb
Simple theorems about zgcd moved to GCD.thy
2008-07-14, by chaieb
Theorem names as in IntPrimes.thy, also several theorems moved from there
2008-07-14, by chaieb
Fixed proofs.
2008-07-14, by chaieb
ProofNode.current
2008-07-14, by wenzelm
command 'redo' no longer available;
2008-07-14, by wenzelm
replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-14, by wenzelm
removed obsolete 'redo' command;
2008-07-14, by wenzelm
removed obsolete history commands;
2008-07-14, by wenzelm
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
2008-07-14, by wenzelm
obsolete (cf. proof_node.ML);
2008-07-14, by wenzelm
removed Isar/proof_history.ML;
2008-07-14, by wenzelm
added further simple interfaces
2008-07-14, by haftmann
simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-14, by haftmann
unified curried gcd, lcm, zgcd, zlcm
2008-07-14, by haftmann
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
instance real_field < field_char_0;
2008-07-11, by huffman
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
2008-07-11, by haftmann
Fract now total; improved code generator setup
2008-07-11, by haftmann
simple inheritance concept
2008-07-11, by haftmann
tuned thyname lookup
2008-07-11, by haftmann
fixed layout
2008-07-11, by haftmann
explicit completions of arities
2008-07-11, by haftmann
tuned order
2008-07-11, by haftmann
antiquotation
2008-07-11, by haftmann
improved code generator setup
2008-07-11, by haftmann
explicit dependency
2008-07-11, by haftmann
class instead of axclass
2008-07-11, by haftmann
tuned import
2008-07-11, by haftmann
separate class dvd for divisibility predicate
2008-07-11, by haftmann
temporarily disable at-sml-dev-p
2008-07-11, by kleing
updated generated file;
2008-07-10, by wenzelm
restart: Isar.init_point;
2008-07-10, by wenzelm
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
2008-07-10, by wenzelm
activated new versions of undo, kill_proof;
2008-07-10, by wenzelm
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
2008-07-10, by wenzelm
added print;
2008-07-10, by wenzelm
added ProofGeneral.isar_kill_proof;
2008-07-10, by wenzelm
added Isar.init_point, Isar.kill;
2008-07-10, by wenzelm
export init_point;
2008-07-10, by wenzelm
added Isar.linear_undo;
2008-07-10, by wenzelm
tuned;
2008-07-10, by wenzelm
tty interaction: do not move point after error;
2008-07-10, by wenzelm
change_lexicons: no verbosity;
2008-07-10, by wenzelm
added Isar.undo, which emulates old-style undo on global tty state;
2008-07-10, by wenzelm
provide old-style undo operation (still unused);
2008-07-10, by wenzelm
added prompt markup;
2008-07-10, by wenzelm
@{lemma}: allow terminal method;
2008-07-10, by wenzelm
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
2008-07-10, by wenzelm
added is_diag;
2008-07-10, by wenzelm
slightly improved @{lemma} (both for latex and ML);
2008-07-10, by wenzelm
misc tuning;
2008-07-10, by wenzelm
Fixed (harmless) typo in closing *}.
2008-07-10, by ballarin
by intro_locales -> ..
2008-07-10, by huffman
instance real_field < field_char_0
2008-07-10, by huffman
remove redundant lemmas about cmod
2008-07-09, by huffman
removed owner;
2008-07-09, by wenzelm
tuned description;
2008-07-09, by wenzelm
changes wrt. gitweb style;
2008-07-09, by wenzelm
style = isabelle (based on gitweb);
2008-07-09, by wenzelm
rearrange instantiations
2008-07-09, by huffman
added get_first;
2008-07-09, by wenzelm
updated generated file;
2008-07-08, by wenzelm
updated generated file;
2008-07-08, by wenzelm
fix more typos
2008-07-08, by huffman
fix another typo
2008-07-08, by huffman
fix typo
2008-07-08, by huffman
updated generated file;
2008-07-08, by wenzelm
global commands: explicit graph;
2008-07-08, by wenzelm
export str_of;
2008-07-08, by wenzelm
clarified code
2008-07-08, by haftmann
exported weaken combinator
2008-07-08, by haftmann
refined arity property concept
2008-07-08, by haftmann
fix: using IntInf.int for SML
2008-07-08, by haftmann
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
removed obsolete touch_child_thys;
2008-07-08, by wenzelm
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
more qualified ThyInfo names;
2008-07-08, by wenzelm
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
2008-07-08, by wenzelm
removed unused href_opt_name;
2008-07-08, by wenzelm
migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware
2008-07-08, by kleing
retired mac-sml-dev.
2008-07-07, by kleing
absolute imports of HOL/*.thy theories
2008-07-07, by haftmann
prefer theorem names without numbers
2008-07-04, by huffman
HOL-NSA
2008-07-04, by huffman
added marginal setup for code generation
2008-07-04, by haftmann
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
2008-07-03, by huffman
removed old NSPrimes, cf. NSA/Examples/;
2008-07-03, by wenzelm
cvsps: back to non-verbose mode;
2008-07-03, by wenzelm
removed old Complex/ex/NSPrimes.thy;
2008-07-03, by wenzelm
maxfiles = 50;
2008-07-03, by wenzelm
more sessions;
2008-07-03, by wenzelm
more precise dependencies for HOL-Word and HOL-NSA;
2008-07-03, by wenzelm
fixed extremely slow proof of Chain_inits_DiffI
2008-07-03, by huffman
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
2008-07-03, by huffman
move proofs of add_left_cancel and add_right_cancel into the correct locale
2008-07-03, by huffman
cvsps -v (verbose);
2008-07-03, by wenzelm
removed nonstandard analysis theories to HOL-NSA
2008-07-03, by huffman
moved theories to HOL/NSA
2008-07-03, by huffman
add HOL-NSA
2008-07-03, by huffman
use patched cvsps to workaround loss of "foo: bar;" log entries;
2008-07-03, by wenzelm
move nonstandard analysis theories to NSA directory
2008-07-03, by huffman
back to default style, which shows files in changelog view;
2008-07-03, by wenzelm
added description;
2008-07-03, by wenzelm
tuned;
2008-07-03, by wenzelm
logrotate setup;
2008-07-03, by wenzelm
redirect stderr as well;
2008-07-03, by wenzelm
output to log file;
2008-07-03, by wenzelm
specific to CVS;
2008-07-03, by wenzelm
Isabelle repository service.
2008-07-03, by wenzelm
ensure hg/.hg/hgrc;
2008-07-03, by wenzelm
hgrc for conversion and web service;
2008-07-03, by wenzelm
provide HGRCPATH, taken from cvs/Admin;
2008-07-03, by wenzelm
code antiquotation roaring ahead
2008-07-03, by haftmann
tuned
2008-07-03, by haftmann
adjusted postprocessort setup
2008-07-03, by haftmann
added lemma antiquotation
2008-07-03, by haftmann
adjusted rep_datatype
2008-07-03, by haftmann
Adapted to changes in perm_simp / swap_simps.
2008-07-03, by berghofe
Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
2008-07-03, by berghofe
Rewrote code to use swap_simps rather than calc_atm (which tends to
2008-07-03, by berghofe
moved HOL-Plain up;
2008-07-02, by wenzelm
rename Doc doc-src;
2008-07-02, by wenzelm
renamed Contents to Dirs to avoid case-conflict with doc/Contents;
2008-07-02, by wenzelm
section -> subsection
2008-07-02, by huffman
convert Isabelle CVS to Mercurial;
2008-07-02, by wenzelm
use begin and end for proofs in locales
2008-07-02, by huffman
exclude Distribution/bin/Isabelle;
2008-07-02, by wenzelm
init_theory: pass name explicitly;
2008-07-02, by wenzelm
replaced datatype category constructivism by is_theory/is_proof;
2008-07-02, by wenzelm
Toplevel.init_theory: pass name explicitly;
2008-07-02, by wenzelm
command: always keep transition, not just as initial status;
2008-07-02, by wenzelm
cached code for code antiquotation
2008-07-02, by haftmann
code antiquotation roaring ahead
2008-07-02, by haftmann
cleaned up some code generator configuration
2008-07-02, by haftmann
tuned;
2008-07-01, by wenzelm
added datatype category;
2008-07-01, by wenzelm
replaced datatype kind by OuterKeyword.category;
2008-07-01, by wenzelm
clean: HOL-Plain;
2008-07-01, by wenzelm
prove lemma finite in context of finite class
2008-07-01, by huffman
added HOL-Plain;
2008-07-01, by wenzelm
explicit identification of toplevel commands, with status etc.;
2008-07-01, by wenzelm
added name_of;
2008-07-01, by wenzelm
added get_id/put_id;
2008-07-01, by wenzelm
(removed Complex/ROOT.ML)
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
tuned
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
put file dependencies on separate lines
2008-07-01, by huffman
range_composition no longer in simp set
2008-07-01, by huffman
remove simp attribute from range_composition
2008-07-01, by huffman
rename INF to INFM
2008-07-01, by huffman
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
2008-07-01, by huffman
remove redundant instance proof finite_po < cpo
2008-07-01, by huffman
remove unused lemma is_lub_Iup'
2008-07-01, by huffman
replace lub (range Y) with (LUB i. Y i)
2008-07-01, by huffman
add file dependencies
2008-07-01, by huffman
universal bifinite domain
2008-07-01, by huffman
isomorphisms between naturals and sums, products, and finite sets
2008-07-01, by huffman
theory of algebraic deflations
2008-07-01, by huffman
theory of eventually-constant sequences
2008-07-01, by huffman
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
2008-07-01, by huffman
rename compact_approx to compact_take
2008-07-01, by huffman
rename approx_pd to pd_take
2008-07-01, by huffman
split Completion.thy from CompactBasis.thy
2008-07-01, by huffman
filemap for CVS -> Mercurial conversion;
2008-06-30, by wenzelm
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
2008-06-30, by huffman
New theory of deflations and embedding-projection pairs
2008-06-30, by huffman
remove unused Cset.thy
2008-06-30, by huffman
added facts to lemma swap_simps and tuned lemma calc_atms
2008-06-30, by urbanc
simplified retrieval of theory names of consts and types
2008-06-30, by haftmann
tagged arities
2008-06-30, by haftmann
HOL-Complex with proof terms
2008-06-30, by haftmann
code generator setup for "int" also works under eta-contraction
2008-06-30, by haftmann
added ML/ml_thms.ML;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
additional ML antiquotations;
2008-06-28, by wenzelm
moved theorem values to ml_thms.ML;
2008-06-28, by wenzelm
Isar theorem values within ML.
2008-06-28, by wenzelm
added ML/ml_thms.ML;
2008-06-28, by wenzelm
updated generated file;
2008-06-28, by wenzelm
allow overlap of minor keywords and commands;
2008-06-28, by wenzelm
include HOL-Plain;
2008-06-28, by wenzelm
tuned args parser (cf. args.ML);
2008-06-28, by wenzelm
replaced simple_text by fully-featured parse_args;
2008-06-28, by wenzelm
tuned nested args parser;
2008-06-28, by wenzelm
@{lemma}: 'by' keyword;
2008-06-28, by wenzelm
ML: improved antiquotations;
2008-06-28, by wenzelm
added macro interface;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
added thm_name, opt_thm_name;
2008-06-28, by wenzelm
adjusted import
2008-06-27, by haftmann
adjusted import
2008-06-27, by haftmann
added a lemma to at_swap_simps
2008-06-27, by urbanc
remove cset theory; define ideal completions using typedef instead of cpodef
2008-06-26, by huffman
Args.theory;
2008-06-26, by wenzelm
added context/theory scanner;
2008-06-26, by wenzelm
Args.context;
2008-06-26, by wenzelm
fix: need to beta/eta normalize
2008-06-26, by krauss
established Plain theory and image
2008-06-26, by haftmann
added dummy citiation
2008-06-26, by haftmann
dropped recdef
2008-06-26, by haftmann
class theory name lookup improved
2008-06-26, by haftmann
modernized specifications;
2008-06-25, by wenzelm
tuned proofs;
2008-06-25, by wenzelm
modernized specifications;
2008-06-25, by wenzelm
modernized specifications;
2008-06-25, by wenzelm
typo
2008-06-25, by urbanc
re-use official outer keywords;
2008-06-25, by wenzelm
scan: prefer command over keyword, allowing lexicons to overlap;
2008-06-25, by wenzelm
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25, by wenzelm
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25, by wenzelm
antiquote: need to quote outer keywords;
2008-06-25, by wenzelm
tuned;
2008-06-25, by wenzelm
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25, by wenzelm
- Equivariance simpset used in proofs of strong induction and inversion
2008-06-25, by berghofe
pprint: back to proper output of markup, with workaround for Poly/ML crash;
2008-06-25, by wenzelm
back to 1.36 (Poly/ML crash!?);
2008-06-24, by wenzelm
updated generated file;
2008-06-24, by wenzelm
less
more
|
(0)
-10000
-1920
+1920
+10000
+30000
tip