Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-1920
+1920
+10000
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.
More lemmas on Gcd/Lcm
2016-07-01, by Manuel Eberl
Conditionally complete lattice of multisets
2016-07-01, by Manuel Eberl
added fundef_cong rule
2016-06-26, by nipkow
misc tuning and modernization;
2016-06-24, by wenzelm
misc tuning and modernization;
2016-06-24, by wenzelm
merged
2016-06-23, by wenzelm
misc tuning and modernization;
2016-06-23, by wenzelm
tuned signature;
2016-06-23, by wenzelm
avoid overlapping equations for gcd, lcm on integers
2016-06-23, by haftmann
compiling implicit instances into companion objects for classes avoids ambiguities
2016-06-23, by haftmann
print statistics; tuned
2016-06-22, by Lars Hupel
adjust job/thread count for new hardware
2016-06-22, by Lars Hupel
report class parameters within instantiation;
2016-06-22, by wenzelm
clarified PIDE markup;
2016-06-22, by wenzelm
tuned;
2016-06-22, by wenzelm
tuned signature;
2016-06-22, by wenzelm
bundle lifting_syntax;
2016-06-22, by wenzelm
tuned;
2016-06-21, by wenzelm
clarified derived bindings (for PIDE reports);
2016-06-21, by wenzelm
clarified rendering (amending ae9330fdbc16);
2016-06-21, by wenzelm
tuned whitespace;
2016-06-21, by wenzelm
merged
2016-06-21, by wenzelm
position information for literal facts;
2016-06-21, by wenzelm
tuned;
2016-06-21, by wenzelm
tuned;
2016-06-21, by wenzelm
Multivariate_Analysis: add continuous_on_vec_lambda
2016-06-21, by hoelzl
Probability: show that measures form a complete lattice
2016-06-16, by hoelzl
move open_Collect_eq/less to HOL
2016-06-15, by hoelzl
move Conditional_Complete_Lattices to Main
2016-06-17, by hoelzl
Probability: introduce Hahn decomposition; use it to clean up Radon_Nikodym
2016-06-15, by hoelzl
Probability: tuned headers; cleanup Radon_Nikodym
2016-06-14, by hoelzl
read Java system properties from ISABELLE_CI_PROPERTIES
2016-06-21, by Lars Hupel
merged
2016-06-20, by wenzelm
misc tuning and modernization;
2016-06-20, by wenzelm
misc tuning and modernization;
2016-06-20, by wenzelm
prefer HOL definitions;
2016-06-20, by wenzelm
tuned proof;
2016-06-20, by wenzelm
misc tuning and modernization;
2016-06-20, by wenzelm
Merged
2016-06-20, by eberlm
Merged
2016-06-17, by eberlm
fps_from_poly → fps_of_poly
2016-06-17, by eberlm
Merged
2016-06-17, by eberlm
Various additions to polynomials, FPSs, Gamma function
2016-06-16, by eberlm
misc tuning and modernization;
2016-06-19, by wenzelm
benchmark build profile
2016-06-19, by Lars Hupel
killed dead code
2016-06-17, by blanchet
avoid runtime warning with discriminators due to 'Code.del_eqn'
2016-06-17, by blanchet
killed deadcode
2016-06-17, by blanchet
be more careful before filtering out chained facts in Sledgehammer
2016-06-17, by blanchet
normalising multiset theorem names
2016-06-17, by fleury
tuned;
2016-06-16, by wenzelm
isabelle update_cartouches -c -t;
2016-06-16, by wenzelm
tuned;
2016-06-16, by wenzelm
Removed instances of ^ from theory markup
2016-06-16, by paulson
Urysohn's lemma, Dugundji extension theorem and many other proofs
2016-06-15, by paulson
non-deprecated char literals for Scala
2016-06-14, by haftmann
explicit resolution of ambiguous dictionaries
2016-06-14, by haftmann
Merge
2016-06-14, by paulson
new results about topology
2016-06-14, by paulson
Merged
2016-06-14, by eberlm
Integration by substitution
2016-06-14, by eberlm
tuned;
2016-06-14, by wenzelm
tuned;
2016-06-13, by wenzelm
Integral form of Gamma function
2016-06-13, by eberlm
Facts about HK integration, complex powers, Gamma function
2016-06-13, by eberlm
tuned
2016-06-13, by Lars Hupel
tuned;
2016-06-13, by wenzelm
tuned;
2016-06-12, by wenzelm
tuned;
2016-06-11, by wenzelm
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2016-06-11, by haftmann
merged
2016-06-11, by Lars Hupel
start moving actual Jenkins build scripts into the repository
2016-06-11, by Lars Hupel
tuned order for isar-ref;
2016-06-11, by wenzelm
clarified;
2016-06-11, by wenzelm
clarified syntax;
2016-06-11, by wenzelm
spelling;
2016-06-11, by wenzelm
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
2016-06-10, by wenzelm
added command 'unbundle';
2016-06-10, by wenzelm
Merge
2016-06-10, by paulson
code to catch exception TERM in blast
2016-06-10, by paulson
merged
2016-06-10, by wenzelm
avoid duplicate Attrib.local_notes in aux. context;
2016-06-10, by wenzelm
proper restore;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
prefer hybrid 'bundle' command;
2016-06-10, by wenzelm
documentation;
2016-06-09, by wenzelm
clarified;
2016-06-09, by wenzelm
support for bundle definition via target;
2016-06-09, by wenzelm
tuned signature;
2016-06-09, by wenzelm
tuned;
2016-06-09, by wenzelm
tuned signature;
2016-06-09, by wenzelm
tuned;
2016-06-09, by wenzelm
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
2016-06-10, by paulson
merged
2016-06-09, by immler
approximation, derivative, and continuity of floor and ceiling
2016-06-09, by immler
remove smt call in Lebesge_Measure
2016-06-09, by hoelzl
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
2016-06-08, by wenzelm
merged
2016-06-08, by wenzelm
NEWS;
2016-06-08, by wenzelm
tuned proofs;
2016-06-08, by wenzelm
provide dynamic facts in static context, to allow use of method_facts during static closure;
2016-06-08, by wenzelm
tuned;
2016-06-08, by wenzelm
clarified signature;
2016-06-07, by wenzelm
less ambitious arguments: thms only, no context declaration;
2016-06-07, by wenzelm
added method operator "use";
2016-06-07, by wenzelm
clarified signature;
2016-06-07, by wenzelm
clean facts more uniformly;
2016-06-07, by wenzelm
expode method_facts via dynamic method context;
2016-06-07, by wenzelm
tuned;
2016-06-07, by wenzelm
generalized bitlen to floor of log
2016-06-08, by immler
repair Unicode mess-up in c493859d4267
2016-06-08, by Andreas Lochbihler
NEWS and CONTRIBUTORS for SPMF
2016-06-08, by Andreas Lochbihler
merged
2016-06-08, by Andreas Lochbihler
import wasysym needed by Rewrite.thy
2016-06-07, by Andreas Lochbihler
add theory of discrete subprobability distributions
2016-06-07, by Andreas Lochbihler
clear distinction between different situations concerning strictness of code equations
2016-06-06, by haftmann
tuned signature
2016-06-06, by haftmann
more correct exception handling
2016-06-06, by haftmann
explicit tagging of code equations de-baroquifies interface
2016-06-06, by haftmann
dropped unused code
2016-06-06, by haftmann
conventional syntax for unit abstractions
2016-06-06, by haftmann
added action "isabelle.select-entity";
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
less redundant exploration of full name space;
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
avoid multiple reports on shared type;
2016-06-06, by wenzelm
updated to recent changes of Poly/ML directory layout;
2016-06-04, by wenzelm
tuned;
2016-06-04, by wenzelm
Integer.lcm normalizes the sign as in HOL/GCD.thy;
2016-06-04, by wenzelm
support for .scala tools;
2016-06-03, by wenzelm
move ennreal and ereal theorems from MFMC_Countable
2016-06-02, by hoelzl
more flexible build_selection;
2016-06-03, by wenzelm
clarified aliases (no warning for duplicates);
2016-06-02, by wenzelm
eliminated pointless alias (no warning for duplicates);
2016-06-02, by wenzelm
avoid warnings on duplicate rules in the given list;
2016-06-02, by wenzelm
avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
2016-06-02, by wenzelm
Hid RBT.filter
2016-06-02, by Manuel Eberl
proper ceil operation;
2016-06-01, by wenzelm
tuned;
2016-06-01, by wenzelm
isabelle components_checksum -u;
2016-06-01, by wenzelm
more documentation;
2016-06-01, by wenzelm
updated to jdk-8u92;
2016-06-01, by wenzelm
merged
2016-06-01, by wenzelm
NEWS;
2016-06-01, by wenzelm
more adhoc overloading;
2016-06-01, by wenzelm
clarified exception -- actually reject denominator = 0;
2016-06-01, by wenzelm
ML pp for Rat.rat;
2016-06-01, by wenzelm
clarified string_of_rat operations;
2016-06-01, by wenzelm
tuned signature;
2016-06-01, by wenzelm
clarified signature;
2016-06-01, by wenzelm
prefer rat numberals;
2016-06-01, by wenzelm
support rat numerals via special antiquotation syntax;
2016-06-01, by wenzelm
tuned signature;
2016-06-01, by wenzelm
tuned;
2016-06-01, by wenzelm
tuned signature;
2016-06-01, by wenzelm
maintain invariant for exported operation;
2016-05-31, by wenzelm
prefer more efficient Poly/ML operations, taking care of sign;
2016-05-31, by wenzelm
ad-hoc overloading for standard operations on type Rat.rat;
2016-05-31, by wenzelm
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
2016-05-31, by wenzelm
Merged
2016-06-01, by eberlm
Tuned code equations for mappings and PMFs
2016-06-01, by eberlm
Added code generation for PMFs
2016-05-31, by eberlm
merged
2016-05-31, by traytel
moved lemma from afp
2016-05-31, by traytel
ignore Maven build products
2016-05-31, by Lars Hupel
added test
2016-05-31, by blanchet
made parsing of monomorphic/polymorphic constants more robust
2016-05-31, by blanchet
more flexible parsing (towards type class support)
2016-05-31, by blanchet
error message
2016-05-31, by blanchet
allow multiple recursive methods to co-exist in order to support mutual recursion;
2016-05-31, by matichuk
apply current morphism to method text before evaluating;
2016-05-30, by matichuk
merged
2016-05-30, by wenzelm
tuned;
2016-05-30, by wenzelm
allow 'for' fixes for multi_specs;
2016-05-30, by wenzelm
unused;
2016-05-30, by wenzelm
clarified check_open_spec / read_open_spec;
2016-05-29, by wenzelm
tuned;
2016-05-28, by wenzelm
clarified 'axiomatization';
2016-05-28, by wenzelm
clarified axiomatization;
2016-05-28, by wenzelm
clarified axiomatization: proper variables (!);
2016-05-28, by wenzelm
explicit check that abstract constructors cannot be part of official interface
2016-05-29, by haftmann
do not export abstract constructors in code_reflect
2016-05-29, by haftmann
added subtheory of longest common prefix
2016-05-29, by nipkow
tuned proofs;
2016-05-27, by wenzelm
tuned proofs;
2016-05-27, by wenzelm
tuned proofs, to allow unfold_abs_def;
2016-05-27, by wenzelm
clarified "unfold" operations;
2016-05-27, by wenzelm
tuned proof;
2016-05-27, by wenzelm
isabelle update_cartouches -c -t;
2016-05-26, by wenzelm
tuned spelling;
2016-05-26, by wenzelm
examples and documentation for code generator time measurements
2016-05-26, by haftmann
optional timing for code generator conversions
2016-05-26, by haftmann
clarified internal interfaces
2016-05-26, by haftmann
tuned
2016-05-26, by haftmann
delegate inclusion of required dictionaries to user-space instead of half-working magic
2016-05-26, by haftmann
corrected closure scope of static_conv_thingol;
2016-05-26, by haftmann
clarified proof context vs. background theory
2016-05-26, by haftmann
explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
2016-05-26, by haftmann
clarified naming conventions and code for code evaluation sandwiches
2016-05-26, by haftmann
clarified names of variants
2016-05-26, by haftmann
added function "prefixes" and some lemmas
2016-05-26, by nipkow
Merge
2016-05-25, by paulson
Merge
2016-05-25, by paulson
moved two theorems
2016-05-25, by paulson
updated proof of Residue Theorem (form Wenda Li)
2016-05-25, by paulson
merged
2016-05-25, by nipkow
renamed suffix(eq)
2016-05-25, by nipkow
updated 'define';
2016-05-25, by wenzelm
merged
2016-05-25, by wenzelm
isabelle update_cartouches -c -t;
2016-05-25, by wenzelm
isabelle update_cartouches -c -t;
2016-05-25, by wenzelm
NEWS: Permutations of a set and randomised folds
2016-05-25, by eberlm
new Isabelle component for CI infastructure
2016-05-24, by Lars Hupel
merged
2016-05-24, by wenzelm
recovered printing of DIM('a) (cf. 899c9c4e4a4c);
2016-05-24, by wenzelm
updated;
2016-05-24, by wenzelm
simplified syntax;
2016-05-24, by wenzelm
clarified syntax category names according to Isabelle/ML/Scala;
2016-05-24, by wenzelm
simplified syntax: Parse.term corresponds to Args.term etc.;
2016-05-24, by wenzelm
clarified syntax categories;
2016-05-24, by wenzelm
cartouche abbreviations work both for " as well;
2016-05-24, by wenzelm
Removed problematic code equation for set_permutations
2016-05-24, by eberlm
Backed out changeset 8230358fab88
2016-05-24, by eberlm
Deleted problematic code equation in Codegenerator_Test
2016-05-24, by eberlm
Merge
2016-05-24, by paulson
New theory for Homeomorphisms
2016-05-24, by paulson
Merge
2016-05-24, by paulson
renamings and new material
2016-05-24, by paulson
new theorem
2016-05-24, by paulson
deleted stray thm command
2016-05-23, by paulson
deleted needless comment
2016-05-23, by paulson
Resolved cyclic dependency of theories
2016-05-24, by eberlm
Merged
2016-05-24, by eberlm
Added set permutations/random permutations
2016-05-24, by eberlm
merged
2016-05-24, by wenzelm
embedded content may be delimited via cartouches;
2016-05-23, by wenzelm
tuned;
2016-05-23, by wenzelm
merged
2016-05-23, by nipkow
renamed prefix* in Library/Sublist
2016-05-23, by nipkow
generate Vampire 4.0 compatible output
2016-05-23, by blanchet
Merge
2016-05-23, by paulson
Lots of new material for multivariate analysis
2016-05-23, by paulson
removed odd cases rule (see also 8cb42cd97579);
2016-05-23, by wenzelm
tuned proofs;
2016-05-23, by wenzelm
tuned document;
2016-05-23, by wenzelm
misc tuning and modernization;
2016-05-23, by wenzelm
proper document source;
2016-05-23, by wenzelm
misc tuning and modernization;
2016-05-23, by wenzelm
merged
2016-05-21, by nipkow
added timing lemmas
2016-05-21, by nipkow
uniformly continuous function extended continuously on closure
2016-05-20, by immler
reduce isUCont to uniformly_continuous_on
2016-05-20, by immler
removed smt proof
2016-05-20, by immler
better handling of veriT's 'unknown' status
2016-05-20, by fleury
Resolved name clash
2016-05-18, by Manuel Eberl
Merged
2016-05-17, by eberlm
Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-17, by eberlm
Library: add partition_on
2016-05-17, by hoelzl
proper consideration of chained facts in 'try0' minimization
2016-05-17, by blanchet
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
2016-05-14, by wenzelm
tuned;
2016-05-14, by wenzelm
toplevel theorem statements support 'if'/'for' eigen-context;
2016-05-14, by wenzelm
reverted accidental commit;
2016-05-14, by wenzelm
eliminated use of empty "assms";
2016-05-13, by wenzelm
more complete theories;
2016-05-13, by wenzelm
common entity definitions within a global or local theory context;
2016-05-12, by wenzelm
clarified heading
2016-05-12, by haftmann
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
2016-05-12, by haftmann
merged
2016-05-12, by wenzelm
avoid spurious fact index, notably in "context begin" (via Bundle.context);
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
expose Sessions.Info in Build.Results
2016-05-12, by Lars Hupel
introduced class topological_group between topological_monoid and real_normed_vector
2016-05-11, by immler
find dynamic facts as well, but static ones are preferred;
2016-05-10, by wenzelm
some slight generalizations
2016-05-10, by immler
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
2016-05-10, by paulson
two new lemmas about segments
2016-05-10, by paulson
Merge
2016-05-09, by paulson
lemmas about dimension, hyperplanes, span, etc.
2016-05-09, by paulson
merged
2016-05-09, by wenzelm
clarified context, notably for internal use of Simplifier;
2016-05-09, by wenzelm
renamings and refinements
2016-05-09, by paulson
move Stirling numbers from AFP/Discrete_Summation
2016-05-04, by hoelzl
the standard While-rule
2016-05-01, by nipkow
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
2016-04-29, by wenzelm
unfold is subject to unfold_abs_def (still inactive);
2016-04-28, by wenzelm
tuned;
2016-04-28, by wenzelm
NEWS;
2016-04-28, by wenzelm
clarified order: params/prems/concl interchangeable with !!/==> proposition;
2016-04-28, by wenzelm
support 'assumes' in specifications, e.g. 'definition', 'inductive';
2016-04-28, by wenzelm
tuned;
2016-04-27, by wenzelm
merged
2016-04-26, by wenzelm
updated subtle side-conditions;
2016-04-26, by wenzelm
some uses of 'obtain' with structure statement;
2016-04-26, by wenzelm
'obtain' supports structured statements (similar to 'define');
2016-04-26, by wenzelm
more portable: GNU find no longer supports "-perm +mode";
2016-04-26, by wenzelm
more uniform operations for structured statements;
2016-04-26, by wenzelm
defs are closed, which leads to proper auto_bind_facts;
2016-04-26, by wenzelm
tuned notation;
2016-04-26, by wenzelm
misc tuning and modernization;
2016-04-26, by wenzelm
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
2016-04-22, by hoelzl
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
2016-04-22, by hoelzl
Linear_Algebra: alternative representation of linear combination
2016-04-22, by hoelzl
Linear_Algebra: move abstract concepts to front
2016-04-22, by hoelzl
merge
2016-04-25, by blanchet
avoid duplicate mixfix messages in '(co)datatype' type name
2016-04-25, by blanchet
generalize code to avoid making assumptions about type variable names
2016-04-25, by blanchet
intermediate definitions and caching in n2m to keep terms small
2016-04-15, by traytel
n2m operates on (un)folds
2016-04-14, by traytel
clarified rendering;
2016-04-25, by wenzelm
old 'def' is legacy;
2016-04-25, by wenzelm
more rigid check of lhs;
2016-04-25, by wenzelm
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
2016-04-25, by wenzelm
eliminated old 'def';
2016-04-25, by wenzelm
added Isar command 'define';
2016-04-24, by wenzelm
within a proof body context, undeclared frees are like global constants;
2016-04-24, by wenzelm
clarified modules;
2016-04-24, by wenzelm
added "balanced" predicate
2016-04-22, by nipkow
fixed code equation for pdivmod, added improved code equation for pseudo_mod
2016-04-20, by Rene Thiemann
proper latex;
2016-04-20, by wenzelm
merged
2016-04-20, by wenzelm
reactivated other_id reports (see also db929027e701, 8eda56033203);
2016-04-20, by wenzelm
invisible context similar to interpretation;
2016-04-20, by wenzelm
avoid massive multiplication of reports due to interpretation;
2016-04-20, by wenzelm
tuned comments;
2016-04-19, by wenzelm
more thorough update;
2016-04-19, by wenzelm
several updates on polynomial long division and pseudo division
2016-04-15, by Rene Thiemann
fragment of a HOL type class primer
2016-04-18, by haftmann
capitalized GCD and LCM syntax
2016-04-18, by haftmann
environment variable check has become pointless after 771b8ad5c7fc
2016-04-18, by haftmann
unfold internal definitions before emitting a proof obligation
2016-04-19, by traytel
more IDE support for Isabelle/Pure bootstrap;
2016-04-19, by wenzelm
merged
2016-04-18, by wenzelm
tuned signature;
2016-04-18, by wenzelm
prefer internal attribute source;
2016-04-18, by wenzelm
tidying some proofs; getting rid of "nonempty_witness"
2016-04-18, by paulson
Merge
2016-04-18, by paulson
numerous theorems about affine hulls, hyperplanes, etc.
2016-04-18, by paulson
merged
2016-04-18, by wenzelm
proper LaTeX;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
avoid clash with function called "x";
2016-04-18, by wenzelm
new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-18, by paulson
clarified bindings;
2016-04-17, by wenzelm
clarified bindings;
2016-04-17, by wenzelm
prefer binding over base name;
2016-04-17, by wenzelm
clarified signature;
2016-04-17, by wenzelm
removed pointless check (see Type_Infer.object_logic);
2016-04-17, by wenzelm
prefer precise names for internal construction;
2016-04-17, by wenzelm
remove "slow" session tags
2016-04-17, by Lars Hupel
misc tuning and modernization;
2016-04-17, by wenzelm
clarified reported positions;
2016-04-17, by wenzelm
operate on proper binding;
2016-04-17, by wenzelm
tuned;
2016-04-17, by wenzelm
add "slow" group to descendants of HOL-Proofs
2016-04-15, by Lars Hupel
merged
2016-04-15, by wenzelm
support for Poly/ML entity ids;
2016-04-15, by wenzelm
clarified PIDE reports;
2016-04-15, by wenzelm
clarified rendering wrt. hyperlinks;
2016-04-15, by wenzelm
tuned -- no position;
2016-04-15, by wenzelm
clarified focus visibility;
2016-04-15, by wenzelm
tuned rendering;
2016-04-15, by wenzelm
highlighting of entity def/ref positions wrt. cursor;
2016-04-14, by wenzelm
background color for entity def/ref focus;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
more silence;
2016-04-14, by wenzelm
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
clarified context;
2016-04-14, by wenzelm
misc tuning and standardization;
2016-04-14, by wenzelm
tuned headers;
2016-04-14, by wenzelm
fix HOL-Probability-ex
2016-04-15, by hoelzl
change is incompatible
2016-04-14, by hoelzl
Probability: move emeasure and nn_integral from ereal to ennreal
2016-04-14, by hoelzl
tuned;
2016-04-14, by wenzelm
clarified modules;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
back to exact copy of non-text file (amending dcc8e1d34b18);
2016-04-14, by wenzelm
merged
2016-04-13, by wenzelm
eliminated "xname" and variants;
2016-04-13, by wenzelm
clarified syntax;
2016-04-13, by wenzelm
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
2016-04-13, by wenzelm
tuned;
2016-04-13, by wenzelm
clarified syntax;
2016-04-13, by wenzelm
avoid quotes for qualified names;
2016-04-13, by wenzelm
added rule
2016-04-13, by immler
tuned;
2016-04-12, by wenzelm
merged
2016-04-12, by wenzelm
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
2016-04-12, by wenzelm
back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
2016-04-12, by wenzelm
Type_Infer.object_logic controls improvement of type inference result;
2016-04-12, by wenzelm
tuned;
2016-04-12, by wenzelm
simplified constraints;
2016-04-11, by wenzelm
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
2016-04-11, by wenzelm
tuned imports;
2016-04-11, by wenzelm
tuned message;
2016-04-11, by wenzelm
tuned;
2016-04-11, by wenzelm
added lemmas
2016-04-12, by immler
generalized
2016-04-12, by immler
added derivative of scaling in exponential function
2016-04-12, by immler
lots of new theorems for multivariate analysis
2016-04-11, by paulson
tuned;
2016-04-10, by wenzelm
tuned;
2016-04-10, by wenzelm
tuned comments;
2016-04-10, by wenzelm
more standard session build process, including browser_info;
2016-04-10, by wenzelm
clarified files;
2016-04-10, by wenzelm
tuned;
2016-04-10, by wenzelm
proper support for recursive ML debugging;
2016-04-10, by wenzelm
tuned -- avoid recoding properties;
2016-04-10, by wenzelm
removed old proof method "default";
2016-04-09, by wenzelm
clean message more thoroughly;
2016-04-09, by wenzelm
clarified modules;
2016-04-09, by wenzelm
avoid interference with running PIDE protocol;
2016-04-09, by wenzelm
proper signature for structure;
2016-04-09, by wenzelm
tuned signature;
2016-04-09, by wenzelm
proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
2016-04-09, by wenzelm
support ROOT0.ML as well -- independently of ROOT.ML;
2016-04-09, by wenzelm
flags as in 'ML' command;
2016-04-09, by wenzelm
shared output primitives of physical/virtual Pure;
2016-04-09, by wenzelm
shared thread position for physical/virtual Pure;
2016-04-09, by wenzelm
prefer Synchronized.var;
2016-04-09, by wenzelm
tuned signature;
2016-04-09, by wenzelm
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
2016-04-09, by wenzelm
tuned signature;
2016-04-09, by wenzelm
tuned signature -- closer to Exn.Interrupt.expose in Scala;
2016-04-09, by wenzelm
clarified bootstrap;
2016-04-09, by wenzelm
clarified context;
2016-04-09, by wenzelm
old;
2016-04-09, by wenzelm
ensure globally unique counter results;
2016-04-09, by wenzelm
tuned;
2016-04-09, by wenzelm
clarified modules;
2016-04-09, by wenzelm
backout 930a30c1a9af: leads to odd effect of command-line options becoming persistent preferences;
2016-04-08, by wenzelm
eliminated ancient TTY-based Tactical.tracify and related global references;
2016-04-08, by wenzelm
updated according to 705d4c4003ea;
2016-04-08, by wenzelm
option "-o" for "isabelle jedit";
2016-04-08, by wenzelm
eliminated unused simproc identifier;
2016-04-08, by wenzelm
section headings for ROOT.ML;
2016-04-07, by wenzelm
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
2016-04-07, by wenzelm
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
2016-04-07, by wenzelm
clarified word syntax: "." is separator or delimiter;
2016-04-07, by wenzelm
clarified mode of ROOT.ML files;
2016-04-07, by wenzelm
(un)folds are not legacy
2016-04-07, by traytel
removed duplicate lemma
2016-04-07, by traytel
derive (co)rec uniformly from (un)fold
2016-04-07, by traytel
NEWS;
2016-04-07, by wenzelm
updated documentation;
2016-04-07, by wenzelm
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
2016-04-07, by wenzelm
unused (see caaa2fc4040d);
2016-04-07, by wenzelm
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-07, by wenzelm
clarified bootstrap of @{make_string} -- avoid query on ML environment;
2016-04-07, by wenzelm
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
2016-04-07, by wenzelm
prefer regular context update, to allow continuous editing of Pure;
2016-04-07, by wenzelm
clarified editor mode;
2016-04-07, by wenzelm
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-06, by wenzelm
more robust bootstrap;
2016-04-06, by wenzelm
virtual thread data via context, for proper support of Context.>> etc;
2016-04-06, by wenzelm
unused;
2016-04-06, by wenzelm
tuned signature;
2016-04-06, by wenzelm
clarified bootstrap;
2016-04-06, by wenzelm
clarified modules;
2016-04-06, by wenzelm
proper return code;
2016-04-06, by wenzelm
clarified ML bootstrap environment;
2016-04-06, by wenzelm
simplified bootstrap: critical structures remain accessible in ML_Root context;
2016-04-06, by wenzelm
more uniform cleanup (via ML_Process in Scala);
2016-04-06, by wenzelm
clarified bootstrap;
2016-04-06, by wenzelm
clarified ML bootstrap;
2016-04-06, by wenzelm
merged
2016-04-05, by wenzelm
proper file extension;
2016-04-05, by wenzelm
clarified files;
2016-04-05, by wenzelm
back to static conditional compilation -- simplified bootstrap;
2016-04-05, by wenzelm
clarified modules -- simplified bootstrap;
2016-04-05, by wenzelm
avoid malformed Isabelle symbols during bootstrap;
2016-04-05, by wenzelm
clarified modules -- simplified bootstrap;
2016-04-05, by wenzelm
clarified bootstrap environment;
2016-04-05, by wenzelm
actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
2016-04-05, by wenzelm
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-05, by wenzelm
tuned;
2016-04-05, by wenzelm
proper syntax;
2016-04-05, by wenzelm
prefer antiquotations;
2016-04-05, by wenzelm
proper use_thy;
2016-04-05, by wenzelm
support for ML project ROOT file, with imitation of ML "use" commands;
2016-04-05, by wenzelm
tuned;
2016-04-05, by wenzelm
read Pure file dependencies directly from ROOT.ML;
2016-04-05, by wenzelm
tuned output;
2016-04-05, by wenzelm
tuned;
2016-04-05, by wenzelm
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
2016-04-05, by traytel
more uniform ML file commands;
2016-04-04, by wenzelm
tuned;
2016-04-04, by wenzelm
tuned;
2016-04-04, by wenzelm
tuned whitespace;
2016-04-04, by wenzelm
tuned headers;
2016-04-04, by wenzelm
merged
2016-04-04, by wenzelm
tuned -- more explicit sections;
2016-04-04, by wenzelm
clarified bootstrap -- avoid conditional compilation in ROOT.ML;
2016-04-04, by wenzelm
allow empty string;
2016-04-04, by wenzelm
tuned;
2016-04-04, by wenzelm
clarified modules;
2016-04-04, by wenzelm
option ML_system_unsafe;
2016-04-04, by wenzelm
clarified conditional compilation;
2016-04-04, by wenzelm
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
2016-04-04, by wenzelm
clarified bootstrap -- more uniform use of ML files;
2016-04-04, by wenzelm
clarified bootstrap;
2016-04-04, by wenzelm
clarified final setup of ML environment;
2016-04-04, by wenzelm
clarified modules;
2016-04-04, by wenzelm
avoid duplicate reports;
2016-04-04, by wenzelm
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-04-04, by paulson
added reference from NEWS to docs
2016-04-04, by blanchet
merged
2016-04-03, by wenzelm
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
2016-04-03, by wenzelm
clarified SML name space: no access to structure PolyML;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
isabelle update_cartouches -c -t;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
prefer internal tool;
2016-04-03, by wenzelm
support for internal tools;
2016-04-03, by wenzelm
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
2016-04-03, by wenzelm
clarified usage;
2016-04-03, by wenzelm
tuned names
2016-04-03, by traytel
prefer infix operations;
2016-04-02, by wenzelm
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
2016-04-02, by wenzelm
proper signature;
2016-04-02, by wenzelm
tuned signature;
2016-04-02, by wenzelm
tuned;
2016-04-02, by wenzelm
tuned signature;
2016-04-02, by wenzelm
proper type;
2016-04-02, by wenzelm
careful export of type-dependent functions, without losing their special status;
2016-04-02, by wenzelm
clarified modules;
2016-04-02, by wenzelm
clarified modules;
2016-04-02, by wenzelm
tuned LaTeX
2016-04-02, by blanchet
import package that might help on some machines (e.g., macbroy2)
2016-04-02, by blanchet
clarified check_sources;
2016-04-02, by wenzelm
obsolete (see 1d977436c1bf);
2016-04-02, by wenzelm
more robust display of bidirectional Unicode text: enforce left-to-right;
2016-04-02, by wenzelm
merged
2016-04-01, by wenzelm
merged
2016-04-01, by wenzelm
explicit warning about bidi uncertainty in Unicode;
2016-04-01, by wenzelm
explicit warning about formal use of Unicode;
2016-04-01, by wenzelm
documentation;
2016-04-01, by wenzelm
more markup;
2016-04-01, by wenzelm
require actual space;
2016-04-01, by wenzelm
tuned signature;
2016-04-01, by wenzelm
required space is already part of Position.here;
2016-04-01, by wenzelm
tuned messages;
2016-04-01, by wenzelm
clarified errors -- disallow cartouche fragments as delimiter;
2016-04-01, by wenzelm
tuned signature;
2016-04-01, by wenzelm
tuned;
2016-04-01, by wenzelm
clarified end position;
2016-04-01, by wenzelm
tuned signature;
2016-04-01, by wenzelm
tuned;
2016-04-01, by wenzelm
removed redundant Position.set_range -- already done in Position.range;
2016-04-01, by wenzelm
lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
2016-04-01, by wenzelm
less bulky timing information, e.g. HOL 56913 ~> 672;
2016-04-01, by wenzelm
tuned;
2016-04-01, by wenzelm
more operations (cf. Scala version);
2016-04-01, by wenzelm
tuned whitespace;
2016-04-01, by wenzelm
explicit property for unbreakable block;
2016-04-01, by wenzelm
unused;
2016-04-01, by wenzelm
tuned markup;
2016-04-01, by wenzelm
clarified treatment of properties;
2016-04-01, by wenzelm
more robust pretty printing: permissive treatment of bad values;
2016-04-01, by wenzelm
adapted to Poly/ML repository version 2e40cadc975a;
2016-04-01, by wenzelm
explicit mixfix block properties;
2016-03-31, by wenzelm
clarified modules;
2016-03-31, by wenzelm
tuned signature;
2016-03-31, by wenzelm
reintroduced check that may guard some tactic failures
2016-04-01, by blanchet
adapt theory names within the theory
2016-04-01, by blanchet
made tactic more robust
2016-03-31, by traytel
tuned interface
2016-03-31, by traytel
merged
2016-03-30, by wenzelm
proper object-logic constraint (amending dd2914250ca7);
2016-03-30, by wenzelm
reconcile object-logic constraint vs. mixfix constraint;
2016-03-30, by wenzelm
more explicit support for object-logic constraint;
2016-03-30, by wenzelm
more language markup;
2016-03-30, by wenzelm
more accurate mixfix type constraints;
2016-03-30, by wenzelm
tuned;
2016-03-30, by wenzelm
tuned message;
2016-03-30, by wenzelm
more explicit type;
2016-03-30, by wenzelm
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
2016-03-30, by wenzelm
avoid duplicate reports;
2016-03-30, by wenzelm
tuned messages -- position is usually missing here;
2016-03-30, by wenzelm
more PIDE markup;
2016-03-30, by wenzelm
clarified modules;
2016-03-30, by wenzelm
clarified errors: more positions;
2016-03-30, by wenzelm
clarified simple mixfix;
2016-03-30, by wenzelm
tuned;
2016-03-30, by wenzelm
more operations;
2016-03-30, by wenzelm
updated dependencies;
2016-03-30, by wenzelm
updated to Navigator 2.6;
2016-03-30, by wenzelm
more 'corec' docs
2016-03-30, by blanchet
merged
2016-03-29, by wenzelm
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
2016-03-29, by wenzelm
tuned messages -- more positions;
2016-03-29, by wenzelm
more position information for type mixfix;
2016-03-29, by wenzelm
tuned signature;
2016-03-29, by wenzelm
proper norm_props, e.g. relevant for ML pp;
2016-03-29, by wenzelm
clarified reports;
2016-03-29, by wenzelm
tuned signature;
2016-03-29, by wenzelm
more 'corec' docs
2016-03-29, by blanchet
tuning
2016-03-29, by blanchet
more 'corec' docs
2016-03-29, by blanchet
try tactics in right order w.r.t. schematics
2016-03-29, by blanchet
more natural order for 'cong_intros'
2016-03-29, by blanchet
more 'corec' documentation
2016-03-29, by blanchet
renamed generated theorem
2016-03-29, by blanchet
tuning
2016-03-29, by blanchet
added sketchy 'corec' documentation
2016-03-29, by blanchet
compile
2016-03-28, by blanchet
updated Sledgehammer documentation
2016-03-28, by blanchet
a more generous hard timeout
2016-03-28, by blanchet
early warning when Sledgehammer finds a proof
2016-03-28, by blanchet
another 'corec' example
2016-03-28, by blanchet
don't ask too much of 'transfer_prover'
2016-03-28, by blanchet
commented out for now
2016-03-28, by blanchet
tuning
2016-03-28, by blanchet
FIXME
2016-03-28, by blanchet
avoid 'prove_sorry' for unreliable tactics
2016-03-28, by blanchet
reused code
2016-03-28, by blanchet
tuning
2016-03-28, by blanchet
tuned examples
2016-03-28, by blanchet
new 'corec' example
2016-03-28, by blanchet
more reliable check for rhs variables
2016-03-28, by blanchet
strengthened tactic
2016-03-28, by blanchet
generalized ML function
2016-03-28, by blanchet
added '_legacy' suffixes
2016-03-28, by blanchet
generalized ML interface
2016-03-28, by blanchet
tuning
2016-03-28, by blanchet
refined experimental option of Sledgehammer
2016-03-28, by blanchet
tuned;
2016-03-26, by wenzelm
explicit print_depth for the sake of Spec_Check.determine_type;
2016-03-26, by wenzelm
obsolete -- done in Isabelle_Process.init_options;
2016-03-26, by wenzelm
clarified use of options;
2016-03-26, by wenzelm
tuned signature;
2016-03-26, by wenzelm
clarified use of options;
2016-03-26, by wenzelm
avoid hardwired values;
2016-03-26, by wenzelm
eliminated duplicate;
2016-03-26, by wenzelm
more operations;
2016-03-26, by wenzelm
merged
2016-03-24, by nipkow
merged
2016-03-24, by nipkow
added Leftist_Heap
2016-03-24, by nipkow
updated to scala-2.11.8;
2016-03-24, by wenzelm
proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
2016-03-24, by wenzelm
more operations;
2016-03-24, by wenzelm
tuned signature;
2016-03-24, by wenzelm
HOL-Word: add stronger bl_to_bin_lt2p_drop
2016-03-23, by kleing
proper sectioning
2016-03-23, by blanchet
sorted out type issue with sort constraints
2016-03-23, by blanchet
tuned whitespace
2016-03-22, by blanchet
compile
2016-03-22, by blanchet
added 'corec' examples and tests
2016-03-22, by blanchet
file header
2016-03-22, by blanchet
added two 'corec' examples
2016-03-22, by blanchet
document addition of 'corec'
2016-03-22, by blanchet
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-22, by blanchet
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
2016-03-22, by blanchet
nicer error
2016-03-22, by blanchet
more debugging
2016-03-22, by blanchet
more general, reliable N2M
2016-03-22, by blanchet
better warning, with definitions in right order
2016-03-22, by blanchet
export ML function
2016-03-22, by blanchet
added timers to N2M
2016-03-22, by blanchet
document that n2m does not depend on most things in fp_sugar in its type
2016-03-22, by traytel
clarified rule structure;
2016-03-21, by wenzelm
accomodate Isabelle identifiers with subscripts;
2016-03-21, by wenzelm
more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
2016-03-21, by wenzelm
eliminated unused argument (see also 58110c1e02bc);
2016-03-21, by wenzelm
add le_log_of_power and le_log2_of_power by Tobias Nipkow
2016-03-21, by hoelzl
unified CHAR with CHR syntax
2016-03-19, by haftmann
isabelle process -T THEORY;
2016-03-18, by wenzelm
proper option -l;
2016-03-18, by wenzelm
avoid redundant addLeftOfScrollBar;
2016-03-18, by wenzelm
no dependency on HighlightPlugin, despite e7b2cfcef94c;
2016-03-18, by wenzelm
observe ML print depth;
2016-03-18, by wenzelm
clarified print depth;
2016-03-18, by wenzelm
recovered from Unicode accident in 7248d106c607;
2016-03-18, by wenzelm
merged
2016-03-18, by wenzelm
tuned -- fewer warnings;
2016-03-18, by wenzelm
discontinued slightly odd "secure" mode;
2016-03-18, by wenzelm
clarified Pretty.T toplevel pp;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
tuned header;
2016-03-18, by wenzelm
clarified modules;
2016-03-18, by wenzelm
@{make_string} is available during Pure bootstrap;
2016-03-17, by wenzelm
clarified modules;
2016-03-17, by wenzelm
unused;
2016-03-17, by wenzelm
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
2016-03-17, by wenzelm
obsolete;
2016-03-17, by wenzelm
tuned signature;
2016-03-17, by wenzelm
obsolete;
2016-03-17, by wenzelm
tuned whitespace;
2016-03-17, by wenzelm
proper ML type;
2016-03-17, by wenzelm
merged
2016-03-18, by Andreas Lochbihler
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-18, by Andreas Lochbihler
superfluous premise (noticed by Julian Nagele)
2016-03-18, by nipkow
added tree lemmas
2016-03-18, by nipkow
normalize schematic names since they are used to instantiate the theorem later
2016-03-18, by traytel
more stuff for extended nonnegative real numbers
2016-03-17, by hoelzl
less preconditions
2016-03-17, by Andreas Lochbihler
merged
2016-03-16, by wenzelm
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
2016-03-16, by wenzelm
pro-forma selection for improved error message;
2016-03-16, by wenzelm
eliminated without magic name;
2016-03-16, by wenzelm
NEWS;
2016-03-16, by wenzelm
always build with full results;
2016-03-16, by wenzelm
clarified name;
2016-03-16, by wenzelm
isabelle process -d;
2016-03-16, by wenzelm
tuned signature;
2016-03-16, by wenzelm
support for Poly/ML heap hierarchy, which saves a lot of disk space;
2016-03-16, by wenzelm
clarified signature;
2016-03-16, by wenzelm
tuned signature;
2016-03-16, by wenzelm
less physical "logic" argument, with option -l like "isabelle console" etc.;
2016-03-16, by wenzelm
find heaps uniformly via Sessions.Store;
2016-03-15, by wenzelm
clarified modules;
2016-03-15, by wenzelm
clarified modules;
2016-03-15, by wenzelm
ML save_state under control of Isabelle/Scala;
2016-03-15, by wenzelm
clarified prompt: "ML" usually means Isabelle/ML;
2016-03-15, by wenzelm
record stamps of cumulative input heaps;
2016-03-14, by wenzelm
Merge
2016-03-16, by paulson
Contractible sets. Also removal of obsolete theorems and refactoring
2016-03-16, by paulson
add measurability rules for ennreal
2016-03-16, by hoelzl
generalized some Borel measurable statements to support ennreal
2016-03-16, by hoelzl
rationalisation of theorem names esp about "real Archimedian" etc.
2016-03-15, by paulson
add fixpoint induction principle
2016-03-15, by Andreas Lochbihler
generalized ML function
2016-03-14, by blanchet
New results about paths, segments, etc. The notion of simply_connected.
2016-03-14, by paulson
Merge
2016-03-14, by paulson
Refactoring (moving theorems into better locations), plus a bit of new material
2016-03-14, by paulson
strengthened tactics
2016-03-14, by blanchet
tuned;
2016-03-13, by wenzelm
tuned signature;
2016-03-13, by wenzelm
prefer Scala over bash function;
2016-03-13, by wenzelm
tuned;
2016-03-13, by wenzelm
clarified env;
2016-03-13, by wenzelm
unused;
2016-03-13, by wenzelm
more uniform signature for various process invocations;
2016-03-13, by wenzelm
tuned;
2016-03-13, by wenzelm
more theorems on orderings
2016-03-13, by haftmann
dropped junk
2016-03-13, by haftmann
tuned;
2016-03-12, by wenzelm
merged
2016-03-12, by wenzelm
tuned;
2016-03-12, by wenzelm
clarified cleanup;
2016-03-12, by wenzelm
more thorough cleanup -- in Scala;
2016-03-12, by wenzelm
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
2016-03-12, by wenzelm
obsolete (cf. 63a5782c764e);
2016-03-12, by wenzelm
clarified session build options: already provided by ML_Process;
2016-03-12, by wenzelm
spelling
2016-03-12, by haftmann
model characters directly as range 0..255
2016-03-12, by haftmann
tuned messages;
2016-03-11, by wenzelm
tuned message;
2016-03-11, by wenzelm
generate theorems like 'bool.split_sel'
2016-03-11, by blanchet
merged
2016-03-10, by wenzelm
tuned;
2016-03-10, by wenzelm
tuned;
2016-03-10, by wenzelm
upgrade "isabelle build" to Isabelle/Scala;
2016-03-10, by wenzelm
prefer plain "isabelle" from PATH within Isabelle settings environment;
2016-03-10, by wenzelm
isabelle_process is superseded by "isabelle process" tool;
2016-03-10, by wenzelm
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
2016-03-10, by wenzelm
clarified modules;
2016-03-10, by wenzelm
clarified files;
2016-03-10, by wenzelm
clarified files;
2016-03-10, by wenzelm
don't throw an exception when trying to print an error message
2016-03-10, by blanchet
eta-expansion done right in "primcorec"
2016-03-10, by blanchet
clarified: constructors in the sense of the code generator are not invertible;
2016-03-10, by haftmann
moved
2016-03-10, by haftmann
merged
2016-03-09, by wenzelm
obsolete;
2016-03-09, by wenzelm
clarified interactive mode, which is relevant for ML prompts;
2016-03-09, by wenzelm
more careful print_depth on startup;
2016-03-09, by wenzelm
ignore SIGINT in waiting wrapper process;
2016-03-09, by wenzelm
more robust cleanup;
2016-03-09, by wenzelm
isabelle.Build uses ML_Process directly;
2016-03-09, by wenzelm
tuned;
2016-03-09, by wenzelm
print timing like lib/scripts/timestop.bash;
2016-03-09, by wenzelm
prefer explicit locale;
2016-03-09, by wenzelm
bash process with builtin timing;
2016-03-09, by wenzelm
elapsed time in milliseconds (cf. Time.now in Poly/ML);
2016-03-09, by wenzelm
support for timing of the managed process;
2016-03-09, by wenzelm
tuned;
2016-03-09, by wenzelm
proper support for RAW_ML_SYSTEM;
2016-03-08, by wenzelm
tuned signature;
2016-03-08, by wenzelm
separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
2016-03-08, by wenzelm
back to external line editor, due to problems of JLine with multithreading of in vs. out;
2016-03-08, by wenzelm
ignore execeptions that usually occur due to shutdown;
2016-03-08, by wenzelm
clarified initial ML;
2016-03-08, by wenzelm
isabelle console is based on Isabelle/Scala;
2016-03-08, by wenzelm
clarified process interrupt: exactly one signal (like thread interrupt);
2016-03-08, by wenzelm
tuned signature;
2016-03-08, by wenzelm
more abstract Session.start, without prover command-line;
2016-03-08, by wenzelm
removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;
2016-03-08, by wenzelm
prospective command line entry point for simplified isabelle_process;
2016-03-07, by wenzelm
tuned signature;
2016-03-07, by wenzelm
proper Path.print for user messages;
2016-03-07, by wenzelm
discontinued cd, pwd;
2016-03-07, by wenzelm
tuned -- more standard operations;
2016-03-07, by wenzelm
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
2016-03-07, by wenzelm
clarified treatment of DEL;
2016-03-07, by wenzelm
clarified RAW_ML_SYSTEM;
2016-03-07, by wenzelm
tuned;
2016-03-07, by wenzelm
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
2016-03-07, by wenzelm
manage the underlying ML process in Scala;
2016-03-07, by wenzelm
clarified modules;
2016-03-07, by wenzelm
tuned signature;
2016-03-07, by wenzelm
Merge
2016-03-09, by paulson
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
2016-03-09, by paulson
explicit record values for dictionary variables
2016-03-08, by haftmann
provide explicit hint concering uniqueness of derivation
2016-03-08, by haftmann
syntax for multiset membership modelled after syntax for set membership
2016-03-08, by haftmann
made 'size' plugin compatible with locales again (and added regression test)
2016-03-07, by blanchet
strengthened tactic
2016-03-07, by blanchet
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
2016-03-07, by paulson
new material to Blochj's theorem, as well as supporting lemmas
2016-03-07, by paulson
merged
2016-03-07, by traytel
less resetting of local theories
2016-03-06, by traytel
avoid redundant escapes;
2016-03-06, by wenzelm
clarified treatment of fragments of Isabelle symbols during bootstrap;
2016-03-06, by wenzelm
clarified ML syntax for strings concerning UTF8;
2016-03-06, by wenzelm
tuned signature;
2016-03-06, by wenzelm
tuned
2016-03-06, by nipkow
NEWS after Isabelle2016;
2016-03-05, by wenzelm
proper latex setup;
2016-03-05, by wenzelm
tuned;
2016-03-05, by wenzelm
abbreviations for \<nexists>;
2016-03-05, by wenzelm
old HOL syntax is for input only;
2016-03-05, by wenzelm
more PIDE markup;
2016-03-05, by wenzelm
tuned signature -- clarified modules;
2016-03-05, by wenzelm
avoid accidental handling of interrupts;
2016-03-05, by wenzelm
unused;
2016-03-05, by wenzelm
tuned signature -- clarified modules;
2016-03-05, by wenzelm
avoid spam in position reports;
2016-03-05, by wenzelm
tuned signature;
2016-03-05, by wenzelm
take qualification of type name more seriously: derived consts and facts are qualified uniformly;
2016-02-26, by wenzelm
merged
2016-03-03, by wenzelm
simplified;
2016-03-03, by wenzelm
obsolete;
2016-03-03, by wenzelm
isabelle console -r" helps to bootstrap Isabelle/Pure;
2016-03-03, by wenzelm
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
2016-03-03, by wenzelm
proper return code (cf. faa452d8e265);
2016-03-03, by wenzelm
clarified isabelle_process;
2016-03-03, by wenzelm
clarified modules;
2016-03-03, by wenzelm
clarified modules;
2016-03-03, by wenzelm
clarified modules;
2016-03-03, by wenzelm
removed junk;
2016-03-03, by wenzelm
discontinued polyml-5.3.0;
2016-03-03, by wenzelm
made Nitpick more robust
2016-03-03, by blanchet
constructive formulation of factorization
2016-03-03, by haftmann
support for ML_exception_debugger;
2016-03-02, by wenzelm
respect qualification when noting theorems in prim(co)rec
2016-03-02, by traytel
added invariant proofs to AA trees
2016-03-02, by nipkow
tuned signature;
2016-03-01, by wenzelm
clarified modules;
2016-03-01, by wenzelm
load secure.ML earlier;
2016-03-01, by wenzelm
clarified modules;
2016-03-01, by wenzelm
clarified modules;
2016-03-01, by wenzelm
ML debugger support in Pure (again, see 3565c9f407ec);
2016-03-01, by wenzelm
use bootstrap compiler earlier;
2016-03-01, by wenzelm
merged
2016-03-01, by wenzelm
merged
2016-03-01, by wenzelm
removed obsolete chmod: isabelle_process no longer supports writable heaps;
2016-03-01, by wenzelm
redundant -- already provided by Poly/ML toplevel;
2016-03-01, by wenzelm
prefer bash_process;
2016-03-01, by wenzelm
only one nested bash process (NB: OS.System = vfork + exec /bin/sh in RTS is faster than Posix.Process.fork/exec in ML);
2016-03-01, by wenzelm
generalized ML function
2016-03-01, by blanchet
tuned bootstrap order to provide type classes in a more sensible order
2016-03-01, by haftmann
missing file;
2016-03-01, by wenzelm
clarified session;
2016-02-29, by wenzelm
tuned header;
2016-02-29, by wenzelm
simplified -- always produce heap for RAW, Pure;
2016-02-29, by wenzelm
merged
2016-02-29, by wenzelm
isabelle_process executable no longer supports writable heap images;
2016-02-29, by wenzelm
more careful cleanup;
2016-02-29, by wenzelm
obsolete;
2016-02-29, by wenzelm
tuned;
2016-02-29, by wenzelm
redundant -- already part of Session.finish;
2016-02-29, by wenzelm
proper exit as in Scala version (in contrast to a45ba78abcc1);
2016-02-29, by wenzelm
save heap more directly;
2016-02-29, by wenzelm
clarified modules;
2016-02-29, by wenzelm
clarified ML heap operations;
2016-02-29, by wenzelm
generalized
2016-02-29, by immler
Merge
2016-02-29, by paulson
Merge
2016-02-29, by paulson
the integral is 0 when otherwise it would be undefined (also for contour integrals)
2016-02-29, by paulson
removed junk;
2016-02-29, by wenzelm
merged
2016-02-28, by wenzelm
clarified;
2016-02-28, by wenzelm
support only polyml-5.3.0 and polyml-5.6;
2016-02-28, by wenzelm
Merged
2016-02-28, by Manuel Eberl
Minor adjustments to euclidean rings
2016-02-28, by Manuel Eberl
proper document source;
2016-02-28, by wenzelm
simplified / unified isatest settings;
2016-02-28, by wenzelm
tuned signature;
2016-02-28, by wenzelm
discontinued old 'header';
2016-02-28, by wenzelm
more official "isabelle check_sources";
2016-02-28, by wenzelm
removed pointless "isabelle yxml";
2016-02-28, by wenzelm
moved getopts to Scala;
2016-02-28, by wenzelm
moved getopts to Scala;
2016-02-28, by wenzelm
obsolete;
2016-02-28, by wenzelm
obsolete;
2016-02-28, by wenzelm
moved getopts to Scala;
2016-02-28, by wenzelm
moved getopts to Scala;
2016-02-28, by wenzelm
tuned;
2016-02-28, by wenzelm
just one File.find_files, based on Java 7 Files operations;
2016-02-28, by wenzelm
More efficient Extended Euclidean Algorithm
2016-02-28, by Manuel Eberl
more symbols;
2016-02-27, by wenzelm
symbol interpretation for \<circle>;
2016-02-27, by wenzelm
update due to fontforge save operation;
2016-02-27, by wenzelm
moved getopts to Scala;
2016-02-27, by wenzelm
moved getopts to Scala;
2016-02-27, by wenzelm
no tracing SPAM, and thus more visible warnings;
2016-02-27, by wenzelm
moved getopts to Scala;
2016-02-27, by wenzelm
tuned messages;
2016-02-27, by wenzelm
more operations (like Markup.parse_bool in ML);
2016-02-27, by wenzelm
tuned messages;
2016-02-27, by wenzelm
support for command-line options as in GNU bash;
2016-02-27, by wenzelm
more succint formulation of membership for multisets, similar to lists;
2016-02-26, by haftmann
Tuned Euclidean Rings/GCD rings
2016-02-26, by Manuel Eberl
Fixed code equations for Gcd/Lcm
2016-02-26, by Manuel Eberl
generalized ML function
2016-02-26, by blanchet
Merged
2016-02-26, by eberlm
Tuned Euclidean Ring instance for polynomials
2016-02-26, by eberlm
Merged
2016-02-26, by eberlm
Merged
2016-02-25, by eberlm
Tuned Euclidean rings
2016-02-25, by eberlm
finite precision computation to determine sign for comparison
2016-02-26, by immler
positive precision for truncate; fixed precision for approximation of rationals; code for truncate
2016-02-26, by immler
compute_real_of_float has not been used as code equation
2016-02-26, by immler
tuned proof;
2016-02-25, by wenzelm
merged
2016-02-25, by wenzelm
slightly more robust re-initialization;
2016-02-25, by wenzelm
isabelle_scala_script is usually found by PATH;
2016-02-25, by wenzelm
within the Isabelle environment, main executables are always within PATH;
2016-02-25, by wenzelm
avoid global state change;
2016-02-25, by wenzelm
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
2016-02-25, by wenzelm
Merge
2016-02-25, by paulson
partial tidy-up of Sylow's theorem
2016-02-25, by paulson
proper option process_output_tail, more generous default;
2016-02-25, by wenzelm
Conformal_mappings: a big development in complex analysis (+ some lemmas)
2016-02-25, by paulson
tuned;
2016-02-25, by wenzelm
tuned signature;
2016-02-25, by wenzelm
proper return code for timeout (amending f868f12f9419);
2016-02-25, by wenzelm
retain tail out_lines as printed, but not the whole log content;
2016-02-25, by wenzelm
explicit class Build_Results;
2016-02-25, by wenzelm
more informative Build.build_results;
2016-02-24, by wenzelm
more informative Process_Result;
2016-02-24, by wenzelm
clarified modules;
2016-02-24, by wenzelm
tuned signature;
2016-02-24, by wenzelm
Merge
2016-02-24, by paulson
Substantial new material for multivariate analysis. Also removal of some duplicates.
2016-02-24, by paulson
NEWS
2016-02-24, by nipkow
refactoring
2016-02-23, by blanchet
merged
2016-02-23, by nipkow
resolved conflict
2016-02-23, by nipkow
more canonical names
2016-02-23, by nipkow
more canonical names
2016-02-23, by nipkow
more canonical names
2016-02-23, by nipkow
merged
2016-02-23, by wenzelm
merged;
2016-02-23, by wenzelm
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
2016-02-23, by wenzelm
avoid outdated Process.interruptConsoleProcesses;
2016-02-22, by wenzelm
tuning
2016-02-23, by blanchet
updated doc
2016-02-23, by blanchet
tuning
2016-02-23, by blanchet
Merge
2016-02-23, by paulson
New and revised material for (multivariate) analysis
2016-02-23, by paulson
was only of historical interest anymore
2016-02-23, by nipkow
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-22, by paulson
generalize more theorems to support enat and ennreal
2016-02-19, by hoelzl
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
2016-02-12, by hoelzl
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-10, by hoelzl
add extended nonnegative real numbers
2016-02-09, by hoelzl
remove lattice syntax from countable complete lattice
2016-02-19, by hoelzl
add countable complete lattices
2016-02-18, by hoelzl
Borel_Space.borel is now in the type class locale
2016-02-09, by hoelzl
add tendsto_add_ereal_nonneg
2016-02-09, by hoelzl
add transfer rule for countable
2016-02-09, by hoelzl
instantiate topologies for nat, int and enat
2016-02-09, by hoelzl
add type class for topological monoids
2016-02-08, by hoelzl
move product topology to HOL-Complex_Main
2016-02-08, by hoelzl
more theorems
2016-02-18, by haftmann
sorted out some duplicate fact bindings
2016-02-18, by haftmann
more direct bootstrap of char type, still retaining the nibble representation for syntax
2016-02-18, by haftmann
moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
2016-02-19, by wenzelm
tutorial is old;
2016-02-19, by wenzelm
tuned
2016-02-19, by nipkow
merged
2016-02-18, by wenzelm
unconditional Multithreading;
2016-02-18, by wenzelm
NEWS concerning 66a381d3f88f
2016-02-18, by haftmann
merged
2016-02-17, by wenzelm
tuned;
2016-02-17, by wenzelm
clarified file names;
2016-02-17, by wenzelm
SML/NJ is no longer supported;
2016-02-17, by wenzelm
dropped various legacy fact bindings and tuned proofs
2016-02-17, by haftmann
separated potentially conflicting type class instance into separate theory
2016-02-17, by haftmann
gcd instances for poly
2016-02-17, by haftmann
more sophisticated GCD syntax
2016-02-17, by haftmann
cleansed junk-producing interpretations for gcd/lcm on nat altogether
2016-02-17, by haftmann
dropped various legacy fact bindings
2016-02-17, by haftmann
generalized some lemmas;
2016-02-17, by haftmann
more theorems concerning gcd/lcm/Gcd/Lcm
2016-02-17, by haftmann
further generalization and polishing
2016-02-17, by haftmann
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
2016-02-17, by haftmann
prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-02-17, by haftmann
consolidated name
2016-02-17, by haftmann
merged
2016-02-17, by wenzelm
removed obsolete RC tags;
2016-02-17, by wenzelm
merged
2016-02-17, by wenzelm
Added tag Isabelle2016 for changeset d3996d5873dd
2016-02-17, by wenzelm
proper syntax;
Isabelle2016
2016-02-15, by wenzelm
tuning
2016-02-17, by blanchet
making 'pred_inject' a first-class BNF citizen
2016-02-17, by blanchet
refactoring
2016-02-17, by blanchet
adjust 112eefe85ff0 to 532ad8de5d61
2016-02-17, by traytel
NEWS
2016-02-17, by traytel
correct (apparently untested) e1698a9578ea
2016-02-17, by traytel
document predicator in datatypes
2016-02-17, by traytel
derive transfer rule for predicator
2016-02-17, by traytel
call the predicator of list list_all
2016-02-17, by traytel
document new 'primrec' feature
2016-02-17, by blanchet
allow predicator instead of map function in 'primrec'
2016-02-17, by blanchet
simp rules for fsts, snds, setl, setr
2016-02-16, by traytel
make predicator a first-class bnf citizen
2016-02-16, by traytel
avoid duplicate theorems in 'primrec's result when invoked programmatically
2016-02-16, by blanchet
tuning
2016-02-15, by blanchet
keep 'ctor_iff_dtor' theorem around in BNF FP database
2016-02-15, by blanchet
tuning
2016-02-15, by blanchet
rephrased message
2016-02-15, by blanchet
clearer error message
2016-02-15, by blanchet
document a limitation of 'primcorec'
2016-02-15, by blanchet
use 'undefined' instead of 'Eps'
2016-02-15, by blanchet
more explicit dummy proofs;
2016-02-14, by wenzelm
more explicit dummy proofs;
2016-02-14, by wenzelm
unused;
2016-02-14, by wenzelm
command '\<proof>' is an alias for 'sorry', with different typesetting;
2016-02-14, by wenzelm
more antiquotations;
2016-02-14, by wenzelm
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
2016-02-14, by wenzelm
tuned whitespace;
2016-02-14, by wenzelm
more careful quoting for the sake of Windows;
2016-02-14, by wenzelm
tuned;
2016-02-14, by wenzelm
tuned;
2016-02-14, by wenzelm
tuned signature;
2016-02-14, by wenzelm
more direct invocation of ISABELLE_BASH_PROCESS on Windows;
2016-02-14, by wenzelm
tuned signature;
2016-02-14, by wenzelm
tuned signature;
2016-02-14, by wenzelm
updated bash_process;
2016-02-13, by wenzelm
actually wait for forked process and return its status -- this is not meant to be a daemon;
2016-02-13, by wenzelm
tuned signature;
2016-02-13, by wenzelm
tuned signature -- more like ML version;
2016-02-13, by wenzelm
suppress empty messages as in ML;
2016-02-13, by wenzelm
clarified bash process -- similar to ML version;
2016-02-13, by wenzelm
clarified bash process;
2016-02-13, by wenzelm
tuned according to ML version;
2016-02-13, by wenzelm
clarified name;
2016-02-13, by wenzelm
more flexible command-line;
2016-02-13, by wenzelm
tuned signature;
2016-02-13, by wenzelm
isabelle update_cartouches -c -t;
2016-02-13, by wenzelm
practically obsolete;
2016-02-13, by wenzelm
obsolete -- no such conditions in main Isabelle repository;
2016-02-13, by wenzelm
tuned header;
2016-02-13, by wenzelm
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
2016-02-13, by wenzelm
unconditional test -- nothing special here;
2016-02-13, by wenzelm
merged
2016-02-12, by wenzelm
Added tag Isabelle2016-RC5 for changeset 45adb8dc84e1
2016-02-12, by wenzelm
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;
2016-02-11, by wenzelm
evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged;
2016-02-11, by wenzelm
tuned;
2016-02-10, by wenzelm
misc tuning;
2016-02-10, by wenzelm
misc tuning and updates;
2016-02-10, by wenzelm
misc tuning and updates;
2016-02-10, by wenzelm
misc tuning;
2016-02-10, by wenzelm
tuned whitespace;
2016-02-10, by wenzelm
more on "Markdown-like text structure";
2016-02-07, by wenzelm
more on 'consider';
2016-02-07, by wenzelm
tuned;
2016-02-07, by wenzelm
more explicit dummy proofs;
2016-02-07, by wenzelm
misc tuning and updates;
2016-02-07, by wenzelm
tuned;
2016-02-07, by wenzelm
clarified old forms;
2016-02-07, by wenzelm
Added tag Isabelle2016-RC4 for changeset f4baefee5776
2016-02-06, by wenzelm
tuned proofs;
2016-02-06, by wenzelm
more on Mac OS X with Retina display;
2016-02-05, by wenzelm
re-init document views for the sake of Text_Overview size;
2016-02-04, by wenzelm
removed unused cancel operation;
2016-02-04, by wenzelm
separate delay_repaint to ensure reactivity, indepently of future_refresh status;
2016-02-04, by wenzelm
suppress ISABELLE_ROOT after init, to avoid conflict with ISABELLE_HOME when folding file names in "isabelle jedit" command-line tool;
2016-02-04, by wenzelm
clarified;
2016-02-04, by wenzelm
recovered handle_resize from 5922db0430f1;
2016-02-04, by wenzelm
preplaying of 'smt' and 'metis' more in sync with actual method
2016-02-01, by blanchet
updated HOL-specific section w.r.t. datatypes
2016-02-01, by blanchet
proper markup for formal text;
2016-02-02, by wenzelm
Added tag Isabelle2016-RC3 for changeset 81cbea2babd9
2016-02-01, by wenzelm
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
2016-02-01, by wenzelm
more on "ML debugging within the Prover IDE";
2016-01-31, by wenzelm
updated to official polyml-5.6;
2016-01-31, by wenzelm
misc tuning and updates;
2016-01-29, by wenzelm
misc tuning and updates;
2016-01-29, by wenzelm
misc tuning;
2016-01-29, by wenzelm
allow single quote within URL;
2016-01-27, by wenzelm
proper try_run for exactly one evaluation of body (amending 91c3aedbfc5e);
2016-01-27, by wenzelm
more thorough syntax_changed: new commands need require new folds;
2016-01-25, by wenzelm
Added tag Isabelle2016-RC2 for changeset 5d513565749e
2016-01-24, by wenzelm
proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;
2016-01-24, by wenzelm
clarified exception handling;
2016-01-24, by wenzelm
guard sessions that no longer work with SML/NJ -- memory problems;
2016-01-24, by wenzelm
tuned signature;
2016-01-24, by wenzelm
tuned;
2016-01-24, by wenzelm
tuned;
2016-01-24, by wenzelm
tuned;
2016-01-24, by wenzelm
proper NEWS for this release;
2016-01-24, by wenzelm
more CONTRIBUTORS;
2016-01-24, by wenzelm
tuned;
2016-01-24, by wenzelm
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
2016-01-24, by wenzelm
back to elementary options used in Isabelle2015 for jdk-7 -- none of the intermediate experiments for jdk-8 improved reactivity on particular dual-CPU system, but the problem seems to be absent on common single-CPU systems;
2016-01-23, by wenzelm
empty abbrevs are removed globally;
2016-01-23, by wenzelm
tuned markup, e.g. relevant for Rendering.tooltip;
2016-01-22, by wenzelm
tuned message;
2016-01-21, by wenzelm
more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized;
2016-01-21, by wenzelm
report error on internal channel as well: startup_failure dialog may be too late;
2016-01-21, by wenzelm
clarified errors: more explicit treatment of uninitialized state;
2016-01-21, by wenzelm
check more files;
2016-01-20, by wenzelm
updated header;
2016-01-20, by wenzelm
tuned text
2016-02-10, by nipkow
tuned
2016-02-09, by nipkow
synchronized with book
2016-02-09, by nipkow
tuned
2016-02-09, by nipkow
avoid error in Isar proof reconstruction if no ATP proof is available
2016-02-01, by blanchet
preplaying of 'smt' and 'metis' more in sync with actual method
2016-02-01, by blanchet
avoid generating polymorphic SPASS constructs to monomorphic SPASS
2016-02-01, by blanchet
Reorganised a huge proof
2016-01-22, by paulson
back to post-release mode -- after fork point;
2016-01-20, by wenzelm
merged
2016-01-20, by wenzelm
bypass input method for better imitation of read-only mode (cf. f26a4d5e82b5): e.g. relevant for composition of ALT-u u on Mac OS X;
2016-01-20, by wenzelm
tuned;
2016-01-20, by wenzelm
clarified -- this is available on Mac OS X, too;
2016-01-20, by wenzelm
updated jdk;
2016-01-20, by wenzelm
tuned signature (according to Scala version);
2016-01-20, by wenzelm
fixed NEWS w.r.t. multisets
2016-01-20, by blanchet
added 'supset' variants for new '<#' etc. symbols on multisets
2016-01-20, by blanchet
added lemma
2016-01-20, by immler
tuned;
2016-01-20, by wenzelm
tuned;
2016-01-19, by wenzelm
tuned
2016-01-19, by nipkow
merged
2016-01-19, by nipkow
added lemma
2016-01-19, by nipkow
Added approximation of powr to NEWS/CONTRIBUTORS
2016-01-19, by Manuel Eberl
Made Approximation work for powr again
2016-01-19, by Manuel Eberl
updated polyml;
2016-01-18, by wenzelm
tuned whitespace;
2016-01-18, by wenzelm
updated mirrors according to website;
2016-01-18, by wenzelm
renamed map_of to lookup
2016-01-17, by nipkow
more method definitions;
2016-01-17, by wenzelm
tuned syntax;
2016-01-16, by wenzelm
tuned;
2016-01-16, by wenzelm
misc tuning and modernization;
2016-01-16, by wenzelm
keep src/Doc;
2016-01-16, by wenzelm
tuned URLs according to website;
2016-01-16, by wenzelm
more symbols;
2016-01-16, by wenzelm
tuned message;
2016-01-16, by wenzelm
tuned message;
2016-01-16, by wenzelm
Added tag Isabelle2016-RC1 for changeset 155d30f721dd
2016-01-15, by wenzelm
misc updates and tuning;
2016-01-15, by wenzelm
misc updates and tuning;
2016-01-15, by wenzelm
misc updates and tuning;
2016-01-15, by wenzelm
continuity of parameterized integral; easier-to-apply formulation of rules
2016-01-15, by immler
tuned;
2016-01-14, by wenzelm
tuned;
2016-01-14, by wenzelm
tuned;
2016-01-14, by wenzelm
made SML/NJ happy;
2016-01-14, by wenzelm
removed dead code;
2016-01-13, by wenzelm
tuned syntax;
2016-01-13, by wenzelm
isabelle update_cartouches -c -t;
2016-01-13, by wenzelm
eliminated spurious Unicode;
2016-01-13, by wenzelm
clarified example;
2016-01-13, by wenzelm
updated section on "Overloaded constant definitions";
2016-01-13, by wenzelm
more doc content;
2016-01-13, by wenzelm
tuned;
2016-01-13, by wenzelm
removed old 'defs' command;
2016-01-13, by wenzelm
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
2016-01-13, by wenzelm
more doc content;
2016-01-13, by wenzelm
merged;
2016-01-13, by wenzelm
tuned signature;
2016-01-13, by wenzelm
proper relative symlink;
2016-01-13, by wenzelm
tuned;
2016-01-13, by wenzelm
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
2016-01-13, by wenzelm
merged
2016-01-13, by nipkow
tuned layout
2016-01-13, by nipkow
updated NEWS
2016-01-13, by blanchet
generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
2016-01-13, by blanchet
more good NEWS;
2016-01-13, by wenzelm
misc tuning and modernization;
2016-01-12, by wenzelm
merged
2016-01-12, by wenzelm
updated old screenshots, added new screenshots;
2016-01-12, by wenzelm
more explicit errors for control symbols that are left-over after Markdown parsing;
2016-01-12, by wenzelm
removed in anticipation of c92d82c3f41b -- demolition after renovation;
2016-01-12, by wenzelm
eliminated old defs;
2016-01-12, by wenzelm
eliminated old defs;
2016-01-12, by wenzelm
clarified axiomatization versus definitions;
2016-01-12, by wenzelm
eliminated old defs;
2016-01-11, by wenzelm
eliminated old defs;
2016-01-11, by wenzelm
eliminated old defs;
2016-01-11, by wenzelm
eliminated old defs;
2016-01-11, by wenzelm
eliminated old defs;
2016-01-11, by wenzelm
eliminated old defs;
2016-01-11, by wenzelm
Deleted problematic code equation in Binomial temporarily.
2016-01-12, by eberlm
add reference
2016-01-12, by Andreas Lochbihler
merged
2016-01-12, by Andreas Lochbihler
add BNF instance for Dlist
2016-01-12, by Andreas Lochbihler
crediting LCP in CONTRIBUTORS
2016-01-12, by paulson
more careful witness' type analysis
2016-01-12, by traytel
removed outdated example
2016-01-12, by traytel
remove unused code
2016-01-12, by matichuk
remove Eisbach's dependency on HOL
2016-01-12, by matichuk
match method now makes proper use of context_tactic
2016-01-11, by matichuk
merged
2016-01-11, by paulson
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
2016-01-11, by paulson
added AA_Map; tuned titles
2016-01-11, by nipkow
tuned
2016-01-11, by nipkow
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2016-01-11, by eberlm
generalized proofs
2016-01-11, by immler
avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables
2016-01-11, by blanchet
tuning
2016-01-11, by blanchet
exported ML function
2016-01-11, by blanchet
setup code generation for filters as suggested by Florian
2016-01-11, by hoelzl
merged
2016-01-11, by Lars Hupel
filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
2016-01-10, by Lukas Bulwahn
isar-ref entry for print_record
2016-01-10, by kleing
add more frequently-run test for print_record
2016-01-10, by kleing
print_record NEWS and CONTRIBUTORS
2016-01-10, by kleing
print_record: diagnostic printing of record definitions
2016-01-10, by kleing
misc tuning and modernization;
2016-01-11, by wenzelm
prune old versions more often, to reduce overall heap requirements;
2016-01-10, by wenzelm
generate HTML version of NEWS, with proper symbol rendering;
2016-01-09, by wenzelm
tuned -- according to ML version;
2016-01-09, by wenzelm
suppress somewhat pointless description (NB: this is displayed in 'print_methods');
2016-01-09, by wenzelm
merged
2016-01-09, by wenzelm
tuned syntax;
2016-01-09, by wenzelm
tuned;
2016-01-09, by wenzelm
\<struct> loses its rendering and is superseded by \<diamondop>;
2016-01-09, by wenzelm
discontinued \<struct> syntax;
2016-01-09, by wenzelm
tuned whitespace;
2016-01-08, by wenzelm
tuned;
2016-01-08, by wenzelm
clarified symbol insertion, depending on buffer encoding;
2016-01-08, by wenzelm
tuned;
2016-01-08, by wenzelm
fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08, by hoelzl
add uniform spaces
2016-01-08, by hoelzl
merged
2016-01-08, by wenzelm
merged
2016-01-08, by wenzelm
tuned;
2016-01-08, by wenzelm
merged
2016-01-08, by wenzelm
more uniform treatment of symblinks: avoid confusion when unpacking .tar.gz bundle with NTFS links;
2016-01-07, by wenzelm
tuned signature;
2016-01-07, by wenzelm
prefer non-ASCII output;
2016-01-07, by wenzelm
more uniform treatment of package internals;
2016-01-07, by wenzelm
more thorough GUI update;
2016-01-07, by wenzelm
tuned;
2016-01-07, by wenzelm
added lemma
2016-01-08, by nipkow
Tuned constant approximations
2016-01-08, by eberlm
merged
2016-01-07, by paulson
revisions to limits and derivatives, plus new lemmas
2016-01-07, by paulson
Added formal power series updates to NEWS/CONTRIBUTORS
2016-01-07, by Manuel Eberl
Tuned approximations in Multivariate_Analysis
2016-01-07, by Manuel Eberl
misc tuning for release;
2016-01-06, by wenzelm
add the proof of the central limit theorem
2016-01-06, by hoelzl
nicer 'Spec_Rules' for size function
2016-01-06, by blanchet
updated docs
2016-01-06, by blanchet
updated NEWS
2016-01-06, by blanchet
more complete setup for 'Rat' in Nitpick
2016-01-06, by blanchet
more systematic treatment of dynamic facts, when forming closure;
2016-01-06, by wenzelm
clarified ROOT files;
2016-01-06, by wenzelm
proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;
2016-01-06, by wenzelm
added ML antiquotation @{method};
2016-01-06, by wenzelm
tuned;
2016-01-05, by wenzelm
tuned;
2016-01-05, by wenzelm
isabelle update_cartouches -c -t;
2016-01-05, by wenzelm
merged
2016-01-05, by wenzelm
more realistic Eisbach method invocation from ML;
2016-01-05, by wenzelm
unused;
2016-01-05, by wenzelm
more robust event propagation;
2016-01-05, by wenzelm
Fixed sectioning in HOL/Library/Polynomial
2016-01-05, by eberlm
Merged
2016-01-05, by eberlm
Added some facts about polynomials
2016-01-05, by eberlm
misc tuning for release;
2016-01-05, by wenzelm
merged
2016-01-05, by wenzelm
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
2016-01-05, by wenzelm
tuned;
2016-01-05, by wenzelm
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
2016-01-05, by eberlm
proper latex setup;
2016-01-05, by wenzelm
updated headers;
2016-01-05, by wenzelm
merged
2016-01-05, by wenzelm
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
2016-01-05, by wenzelm
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
2016-01-05, by hoelzl
merged
2016-01-04, by wenzelm
tuned proofs;
2016-01-04, by wenzelm
node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
2016-01-04, by wenzelm
stop dummy sessions as well;
2016-01-04, by wenzelm
clarified order of shutdown;
2016-01-04, by wenzelm
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2016-01-04, by eberlm
retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);
2016-01-03, by wenzelm
proper treatment of RAW bootstrap session;
2016-01-03, by wenzelm
tuned whitespace;
2016-01-03, by wenzelm
more symbols;
2016-01-02, by wenzelm
tuned spacing of \<partial>;
2016-01-02, by wenzelm
eliminated somewhat pointless and obscure options;
2016-01-02, by wenzelm
isabelle update_cartouches -c -t;
2016-01-02, by wenzelm
tuned;
2016-01-02, by wenzelm
proper platform_path for Windows;
2016-01-02, by wenzelm
clarified isabelle jedit command-line;
2016-01-02, by wenzelm
tuned;
2016-01-02, by wenzelm
avoid downloading contrib again;
2016-01-02, by wenzelm
provide server name uniformly on all platforms;
2016-01-02, by wenzelm
more symbols;
2016-01-02, by wenzelm
NEWS;
2016-01-02, by wenzelm
keep platform bundle for reference, e.g. for headless installation;
2016-01-01, by wenzelm
keep generic archive for all platforms -- required for Admin/Release/build_library;
2016-01-01, by wenzelm
oops;
2016-01-01, by wenzelm
Added tag Isabelle2016-RC0 for changeset e18444532fce
2016-01-01, by wenzelm
tuned;
2016-01-01, by wenzelm
updated for release;
2016-01-01, by wenzelm
tuned;
2016-01-01, by wenzelm
more symbols;
2016-01-01, by wenzelm
clarified abbrev;
2016-01-01, by wenzelm
clarified meaning of \<^bold> action, depending on group;
2016-01-01, by wenzelm
clarified groups, notably for Symbols dockable;
2016-01-01, by wenzelm
glyphs for \<bind>, \<then>;
2016-01-01, by wenzelm
tuned order for isar-ref;
2016-01-01, by wenzelm
isabelle update_cartouches -c -t;
2016-01-01, by wenzelm
updated for release;
2015-12-31, by wenzelm
updated to SML/NJ 110.79;
2015-12-31, by wenzelm
misc tuning for release;
2015-12-31, by wenzelm
misc updates for release;
2015-12-31, by wenzelm
expand hard tabs;
2015-12-31, by wenzelm
documentation for "isabelle jedit_client";
2015-12-31, by wenzelm
discontinued documentation of old browser;
2015-12-31, by wenzelm
more precise context -- potentially relevant for Eisbach dummy thm;
2015-12-31, by wenzelm
tuned;
2015-12-31, by wenzelm
updated sumatra_pdf;
2015-12-31, by wenzelm
clarified imports;
2015-12-31, by wenzelm
clarified directory structure;
2015-12-31, by wenzelm
updated isabelle_fonts;
2015-12-31, by wenzelm
proper diamond from lasy10;
2015-12-31, by wenzelm
modernized defs;
2015-12-31, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
isabelle update_cartouches -c -t;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
updated print modes;
2015-12-30, by wenzelm
modernized Isabelle document markup;
2015-12-30, by wenzelm
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
removed junk;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
isabelle update_cartouches -c -t;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
clarified syntax;
2015-12-30, by wenzelm
clarified print modes;
2015-12-30, by wenzelm
proper latex setup;
2015-12-30, by wenzelm
proper latex setup;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
isabelle update_cartouches -c -t;
2015-12-30, by wenzelm
tuned java options;
2015-12-30, by wenzelm
more symbols;
2015-12-30, by wenzelm
simplified abbrevs: exploit ambiguity;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
avoid immediate completion as ASCII versions that are still used;
2015-12-29, by wenzelm
tuned order for isar-ref manual;
2015-12-29, by wenzelm
more symbols;
2015-12-29, by wenzelm
updated isabelle_fonts;
2015-12-29, by wenzelm
more arrow symbols;
2015-12-29, by wenzelm
more arrow symbols;
2015-12-29, by wenzelm
eliminated obscure macro that is in conflict with amsmath.sty;
2015-12-29, by wenzelm
more abbrevs;
2015-12-29, by wenzelm
support additional abbrevs;
2015-12-29, by wenzelm
tuned;
2015-12-29, by wenzelm
isabelle console: print mode "ASCII";
2015-12-29, by wenzelm
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-29, by wenzelm
more symbols;
2015-12-28, by wenzelm
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28, by wenzelm
more symbols;
2015-12-28, by wenzelm
use symbols by default;
2015-12-28, by wenzelm
prefer symbols for "Union", "Inter";
2015-12-28, by wenzelm
clarified position information;
2015-12-28, by wenzelm
suppress irrelevant position reports;
2015-12-28, by wenzelm
suppress irrelevant position reports;
2015-12-28, by wenzelm
tuned;
2015-12-28, by wenzelm
more position information;
2015-12-28, by wenzelm
put example into separate session, to restrict precious session image to library theories
2015-12-27, by haftmann
more symbols;
2015-12-28, by wenzelm
prefer symbols for "abs";
2015-12-28, by wenzelm
discontinued ASCII replacement syntax <*>;
2015-12-27, by wenzelm
prefer symbols for "floor", "ceiling";
2015-12-27, by wenzelm
discontinued ASCII replacement syntax <->;
2015-12-27, by wenzelm
more symbols;
2015-12-27, by wenzelm
tuned document;
2015-12-27, by wenzelm
more proofs;
2015-12-27, by wenzelm
tuned;
2015-12-27, by wenzelm
more notation;
2015-12-26, by wenzelm
clarified sessions;
2015-12-26, by wenzelm
tuned;
2015-12-26, by wenzelm
isabelle update_cartouches -c -t;
2015-12-26, by wenzelm
misc tuning and modernization;
2015-12-26, by wenzelm
more proofs, more text;
2015-12-26, by wenzelm
modernized example;
2015-12-26, by wenzelm
tuned proofs and augmented lemmas
2015-12-24, by haftmann
tuned proof
2015-12-24, by haftmann
less ambitious test;
2015-12-23, by wenzelm
tuned;
2015-12-23, by wenzelm
clarified directory structure;
2015-12-23, by wenzelm
updated polyml;
2015-12-23, by wenzelm
clarified context policy to allow multiple dummies;
2015-12-23, by wenzelm
NEWS;
2015-12-23, by wenzelm
tuned;
2015-12-23, by wenzelm
merged
2015-12-23, by wenzelm
tuned module arrangement;
2015-12-23, by wenzelm
tuned module arrangement;
2015-12-23, by wenzelm
check and report source at most once, notably in body of "match" method;
2015-12-23, by wenzelm
transfer rule for bounded_linear of blinfun
2015-12-23, by immler
theory for type of bounded linear functions; differentiation under the integral sign
2015-12-22, by immler
stripped some legacy
2015-12-22, by haftmann
tuned proofs and augmented some lemmas
2015-12-22, by haftmann
more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
2015-12-22, by wenzelm
proper full name within the name space of the method definition;
2015-12-22, by wenzelm
tuned signature;
2015-12-22, by wenzelm
isabelle update_cartouches -c -t;
2015-12-22, by wenzelm
Merge
2015-12-22, by paulson
Liouville theorem, Fundamental Theorem of Algebra, etc.
2015-12-22, by paulson
Weierstrass: whitespace
2015-12-22, by hoelzl
merged
2015-12-22, by wenzelm
more thorough event propagation;
2015-12-22, by wenzelm
tuned -- with subtle change of order of evaluation;
2015-12-22, by wenzelm
more accurate lookup of dynamic facts;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
tuned signature;
2015-12-22, by wenzelm
tuned;
2015-12-22, by wenzelm
Bochner integral: prove dominated convergence at_top
2015-12-21, by hoelzl
dead code;
2015-12-21, by wenzelm
tuned spelling;
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
misc tuning and modernization;
2015-12-21, by wenzelm
merged
2015-12-21, by haftmann
documentation on last state of the art concerning interpretation
2015-12-19, by haftmann
abandoned attempt to unify sublocale and interpretation into global theories
2015-12-19, by haftmann
updated Cygwin (somewhere after 1.7.35-1);
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
merged
2015-12-21, by wenzelm
tuned message;
2015-12-21, by wenzelm
more explicit ML profiling, with official Isabelle output;
2015-12-21, by wenzelm
discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-12-21, by wenzelm
clarified length of block with pre-existant forced breaks;
2015-12-21, by wenzelm
Probability: fix coercions (real ~> real_of_enat)
2015-12-21, by hoelzl
Transcendental: use [simp]-canonical form - (pi/2)
2015-12-21, by hoelzl
moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-17, by hoelzl
tuned whitespace;
2015-12-20, by wenzelm
tuned signature;
2015-12-20, by wenzelm
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-12-20, by wenzelm
proper formatting via Pretty.string_of;
2015-12-20, by wenzelm
unused;
2015-12-20, by wenzelm
tuned;
2015-12-20, by wenzelm
prune old document versions more frequently, for reduced heap usage;
2015-12-19, by wenzelm
merged
2015-12-19, by wenzelm
more explicit Pretty.Tree, like in ML;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
clarified underlying datatypes;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
prefer default focus policy, like Output dockable;
2015-12-19, by wenzelm
tuned;
2015-12-19, by wenzelm
tuned signature;
2015-12-19, by wenzelm
support for blocks with consistent breaks;
2015-12-19, by wenzelm
preserve break indentation;
2015-12-19, by wenzelm
support pretty break indent, like underlying ML systems;
2015-12-17, by wenzelm
register record functions as 'Spec_Rules'
2015-12-19, by blanchet
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
2015-12-19, by blanchet
removed subsumed dependency
2015-12-19, by blanchet
removed dead code
2015-12-19, by blanchet
add serialisation for abs on integer to target language operation
2015-12-18, by Andreas Lochbihler
add gcd instance for integer and serialisation to target language operations
2015-12-18, by Andreas Lochbihler
merged
2015-12-16, by wenzelm
tuned whitespace;
2015-12-16, by wenzelm
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-16, by wenzelm
tuned signature -- clarified modules;
2015-12-15, by wenzelm
unused;
2015-12-15, by wenzelm
unused;
2015-12-15, by wenzelm
Merge
2015-12-15, by paulson
New complex analysis material
2015-12-15, by paulson
infix syntax for measurable set
2015-11-25, by hoelzl
more standard term equality;
2015-12-14, by wenzelm
tuned;
2015-12-14, by wenzelm
tuned signature;
2015-12-14, by wenzelm
tuned message;
2015-12-14, by wenzelm
merged
2015-12-13, by wenzelm
more general types Proof.method / context_tactic;
2015-12-13, by wenzelm
tuned;
2015-12-12, by wenzelm
clarified ML scopes;
2015-12-12, by wenzelm
clarified ML scopes;
2015-12-12, by wenzelm
tuned;
2015-12-12, by wenzelm
unused;
2015-12-12, by wenzelm
tuned;
2015-12-12, by wenzelm
clarified modules;
2015-12-11, by wenzelm
modernized
2015-12-12, by haftmann
modernized
2015-12-12, by haftmann
modernized
2015-12-11, by haftmann
isabelle update_cartouches -c -t;
2015-12-10, by wenzelm
proper checksum for cygwin-20151210.tar.gz (some snapshot after 1.7.35-1);
2015-12-10, by wenzelm
avoid application spurious startup error;
2015-12-10, by wenzelm
current Cygwin snapshot in preparation of release;
2015-12-10, by wenzelm
hardwired LANG, to avoid sporadic surprises with local environments;
2015-12-10, by wenzelm
make SML/NJ happy;
2015-12-10, by wenzelm
not_leE -> not_le_imp_less and other tidying
2015-12-10, by paulson
clarified terminology
2015-12-07, by haftmann
tuned;
2015-12-09, by wenzelm
tuned signature;
2015-12-09, by wenzelm
tuned signature;
2015-12-09, by wenzelm
tuned;
2015-12-09, by wenzelm
more direct use of Token.src as token list;
2015-12-09, by wenzelm
merged
2015-12-09, by wenzelm
unused;
2015-12-09, by wenzelm
merged
2015-12-09, by wenzelm
clarified type Token.src: plain token list, with usual implicit value assignment;
2015-12-09, by wenzelm
tuned;
2015-12-09, by wenzelm
tuned;
2015-12-08, by wenzelm
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
2015-12-08, by wenzelm
sorted out eventually_mono
2015-12-09, by paulson
tightened invariant
2015-12-08, by nipkow
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
Merge
2015-12-07, by paulson
Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-12-07, by paulson
Merged
2015-12-07, by eberlm
Generalised derivative rule for division on formal power series
2015-12-07, by eberlm
tuned;
2015-12-07, by wenzelm
more thorough update request: semantic state of command may have changed elsewise;
2015-12-07, by wenzelm
tuned signature;
2015-12-07, by wenzelm
tuned whitespace;
2015-12-07, by wenzelm
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
isabelle update_cartouches -c -t;
2015-12-07, by wenzelm
tuned;
2015-12-07, by wenzelm
tuned;
2015-12-06, by wenzelm
updated to polyml-5.6-20151206, which presumably improves stability on Windows;
2015-12-06, by wenzelm
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
2015-12-06, by wenzelm
added AA trees
2015-12-06, by nipkow
tuned
2015-12-06, by nipkow
tuned
2015-12-05, by nipkow
avoid name clashes
2015-12-05, by nipkow
added Brother12_Map
2015-12-05, by nipkow
tuned docs
2015-12-04, by blanchet
more documentation on 'size' plugin
2015-12-04, by blanchet
nicer error when the given size function has the wrong type
2015-12-04, by blanchet
merged
2015-12-04, by nipkow
added 1-2 brother trees
2015-12-04, by nipkow
updated SMT certificates
2015-12-04, by blanchet
removed needless complication for modern SMT solvers
2015-12-04, by blanchet
tuned language
2015-12-03, by haftmann
moved section according to supposed order of interest
2015-12-03, by haftmann
consolidated documentation
2015-12-03, by haftmann
modernized
2015-12-03, by haftmann
tuned sections
2015-12-03, by haftmann
modernized
2015-12-02, by haftmann
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
2015-12-02, by haftmann
prefer conventional read/check distinction over manual check
2015-12-02, by haftmann
clarified role of context for reading rewrite specifications
2015-12-02, by haftmann
formally correct context for export, which got screwed up in 87203a0f0041
2015-12-02, by haftmann
tuned whitespace
2015-12-02, by haftmann
removed needless ML function
2015-12-01, by blanchet
tuned whitespace
2015-12-01, by blanchet
reverted inadvertently qfinished/pushed change r164eeb2ab675
2015-12-01, by blanchet
merged
2015-12-01, by Andreas Lochbihler
add formalisation of Bourbaki-Witt fixpoint theorem
2015-12-01, by Andreas Lochbihler
add lemmas
2015-12-01, by Andreas Lochbihler
strengthen lemma
2015-12-01, by Andreas Lochbihler
Merge
2015-12-01, by paulson
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-12-01, by paulson
set "transfer_rule" attribute more generously
2015-12-01, by blanchet
tuned whitespace
2015-12-01, by blanchet
misc tuning and modernization;
2015-11-30, by wenzelm
misc tuning and modernization;
2015-11-30, by wenzelm
tuned;
2015-11-30, by wenzelm
avoid 'hence' and 'thus' in generated proofs
2015-11-30, by blanchet
removed tracing
2015-11-30, by blanchet
RBT invariants for insert
2015-11-29, by nipkow
removed junk;
2015-11-28, by wenzelm
merged
2015-11-27, by wenzelm
more reactive GUI;
2015-11-27, by wenzelm
tuned;
2015-11-27, by wenzelm
paint root black after insert and delete
2015-11-27, by nipkow
observe option "indent";
2015-11-25, by wenzelm
more scalable GUI;
2015-11-24, by wenzelm
paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
2015-11-24, by wenzelm
Ported old example to use (co)datatypes
2015-11-24, by traytel
discontinued Mac OS X 10.7 Lion (macbroy6);
2015-11-23, by wenzelm
merged
2015-11-23, by wenzelm
clarified font: GUI defaults might change dynamically;
2015-11-23, by wenzelm
updated platform baseline to Mac OS X 10.8 Mountain Lion;
2015-11-23, by wenzelm
updated to polyml-5.6-20151123;
2015-11-23, by wenzelm
Merge
2015-11-23, by paulson
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-23, by paulson
bundle main sources read-only, to avoid accidental editing of imported theories etc.;
2015-11-23, by wenzelm
more symbols;
2015-11-22, by wenzelm
some GC options that potentially improve reactivity;
2015-11-22, by wenzelm
more thorough completion rendering, e.g. "Un";
2015-11-22, by wenzelm
tuned;
2015-11-22, by wenzelm
Updates to the revision history of the locales tutorial.
2015-11-21, by ballarin
Clarify locale qualifiers: output and tutorial.
2015-11-21, by ballarin
tuned proofs;
2015-11-21, by wenzelm
tuned;
2015-11-21, by wenzelm
double flush to ensure persistent "state" output is reset;
2015-11-21, by wenzelm
reverted 2abbe7d700e9: "state" output is not necessarily proof state;
2015-11-21, by wenzelm
clarified default (again) in accordance to with Output dockable, despite more CPU resources requirements;
2015-11-21, by wenzelm
more thorough update of options;
2015-11-21, by wenzelm
limit statistics, to avoid exhaustion of heap space or GUI time;
2015-11-21, by wenzelm
render snapshot.is_outdated in text overview, where other status information is shown already;
2015-11-21, by wenzelm
avoid flashing of main text area (visual "grey-out") due to spurious edits, e.g. State panel auto-update;
2015-11-21, by wenzelm
clarified default;
2015-11-21, by wenzelm
recovered auto update from f9aaca00be49;
2015-11-21, by wenzelm
less intrusive rendering, notably for State dockable;
2015-11-21, by wenzelm
clarified rendering of Markup.DOC: like Markup.PATH / Markup.URL;
2015-11-21, by wenzelm
more direct access to option "editor_output_state";
2015-11-21, by wenzelm
tuned;
2015-11-21, by wenzelm
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
2015-11-20, by wenzelm
Now just a few seconds faster
2015-11-20, by paulson
merged
2015-11-20, by nipkow
tuned
2015-11-20, by nipkow
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
2015-11-20, by paulson
merged
2015-11-20, by nipkow
tuned
2015-11-20, by nipkow
explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
2015-11-19, by haftmann
tuned;
2015-11-19, by wenzelm
tuned whitespace;
2015-11-19, by wenzelm
trim lines for @{theory_text} similarly to @{text};
2015-11-19, by wenzelm
tuned;
2015-11-19, by wenzelm
tuned and converted to cmp
2015-11-19, by nipkow
misc. changes to Imperative-HOL from Peter Gammie
2015-11-19, by Lars Hupel
Refine the supression of abbreviations for morphisms that are not identities.
2015-11-18, by ballarin
Merge
2015-11-18, by paulson
New theorems mostly from Peter Gammie
2015-11-18, by paulson
make SML/NJ happy;
2015-11-18, by wenzelm
converted to cmp
2015-11-18, by nipkow
moved lemmas
2015-11-18, by nipkow
derive lemmas uniformly
2015-11-17, by nipkow
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-17, by paulson
converted lookup to cmp
2015-11-17, by nipkow
removed lemmas that were only needed for old version of isin.
2015-11-17, by nipkow
clarified contexts by factoring out reading and definition of mixins
2015-11-16, by haftmann
merged
2015-11-16, by Andreas Lochbihler
export internal definition
2015-11-16, by Andreas Lochbihler
corrected inefficient implementation
2015-11-16, by nipkow
more tracing in MaSh
2015-11-16, by blanchet
tuned names
2015-11-16, by nipkow
NEWS
2015-11-16, by nipkow
formally correct context for export
2015-11-15, by haftmann
merged
2015-11-15, by wenzelm
merged
2015-11-15, by wenzelm
option "inductive_defs" controls exposure of def and mono facts;
2015-11-15, by wenzelm
tuned message;
2015-11-14, by wenzelm
added pretty syntax
2015-11-15, by nipkow
tuned white space
2015-11-15, by nipkow
leftover from 27ca6147e3b3
2015-11-15, by haftmann
tuned whitespace
2015-11-15, by haftmann
NEWS
2015-11-15, by haftmann
droppen diagnostic junk from 4b53042d7a40
2015-11-15, by haftmann
represent both algebraic and local-theory views on locale interpretation in interfaces
2015-11-14, by haftmann
tuned -- share implementations as far as appropriate
2015-11-14, by haftmann
prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14, by haftmann
coalesce permanent_interpretation.ML with interpretation.ML
2015-11-14, by haftmann
separate ML module for interpretation
2015-11-14, by haftmann
reverted half-baken 7d1127ac2251
2015-11-14, by haftmann
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
2015-11-14, by haftmann
more standard ML, to make SML/NJ more happy;
2015-11-14, by wenzelm
tuned;
2015-11-13, by wenzelm
tuned whitespace;
2015-11-13, by wenzelm
tuned;
2015-11-13, by wenzelm
tuned whitespace;
2015-11-13, by wenzelm
merged
2015-11-13, by wenzelm
added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-13, by wenzelm
preserve names of for-fixes for faithfully;
2015-11-13, by wenzelm
more documentation;
2015-11-13, by wenzelm
tuned whitespace;
2015-11-13, by wenzelm
more uniform jEdit properties;
2015-11-13, by wenzelm
avoid vacuous quantification, as usual for shared variable scope;
2015-11-13, by wenzelm
support for structure statements in 'assume', 'presume';
2015-11-13, by wenzelm
support short form for \<^theory_text>;
2015-11-12, by wenzelm
MIR decision procedure again working
2015-11-13, by paulson
unnecessary precondition
2015-11-13, by nipkow
Merge
2015-11-13, by paulson
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-13, by paulson
tuned name
2015-11-13, by nipkow
tuned
2015-11-13, by nipkow
use cartouches instead of backquotes
2015-11-12, by blanchet
translation for conjunctive premises
2015-11-12, by nipkow
tuned
2015-11-12, by nipkow
added proof state output warning
2015-11-12, by nipkow
tuned
2015-11-11, by nipkow
merged
2015-11-11, by nipkow
no CRLF
2015-11-11, by nipkow
new conversion theorems for int, nat to float
2015-11-11, by paulson
merged
2015-11-11, by nipkow
uniform proof of lemmas
2015-11-11, by nipkow
merged
2015-11-11, by Andreas Lochbihler
adapt to 90f54d9e63f2
2015-11-11, by Andreas Lochbihler
add various lemmas
2015-11-11, by Andreas Lochbihler
add lemmas
2015-11-11, by Andreas Lochbihler
generalise lemma
2015-11-11, by Andreas Lochbihler
add lemmas for extended nats and reals
2015-11-11, by Andreas Lochbihler
add various lemmas
2015-11-11, by Andreas Lochbihler
cancel complementary terms as arguments to sup/inf in boolean algebras
2015-11-11, by Andreas Lochbihler
add lemmas about monoids and groups
2015-11-11, by Andreas Lochbihler
tuned
2015-11-11, by nipkow
recovered from a9c0572109af;
2015-11-10, by wenzelm
merged
2015-11-10, by wenzelm
tuned whitespace;
2015-11-10, by wenzelm
added @{command}, @{method}, @{attribute};
2015-11-10, by wenzelm
smart quoting of non-identifiers, e.g. jEdit actions;
2015-11-10, by wenzelm
more thorough check_action, including completion;
2015-11-10, by wenzelm
tuned signature;
2015-11-10, by wenzelm
clarified modules;
2015-11-10, by wenzelm
more thorough check_command, including completion;
2015-11-10, by wenzelm
clarified modules;
2015-11-10, by wenzelm
unused;
2015-11-10, by wenzelm
ignore pointless/unused options;
2015-11-10, by wenzelm
added document antiquotation @{theory_text};
2015-11-10, by wenzelm
allow open symboloid;
2015-11-10, by wenzelm
generalized so that is also works for veriT proofs
2015-11-10, by fleury
fixing premises in veriT proof reconstruction
2015-11-10, by fleury
Merge
2015-11-10, by paulson
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-10, by paulson
subdegree/shift/cutoff and Euclidean ring instance for formal power series
2015-11-10, by eberlm
prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply;
2015-11-09, by wenzelm
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
2015-11-09, by wenzelm
qualifier is mandatory by default;
2015-11-09, by wenzelm
prefer explicit State panel;
2015-11-09, by wenzelm
suppress already persistent state output as well;
2015-11-09, by wenzelm
added option timeout_scale;
2015-11-08, by wenzelm
syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML;
2015-11-07, by wenzelm
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-07, by wenzelm
tuned;
2015-11-07, by wenzelm
less confusing markup;
2015-11-07, by wenzelm
added @{undefined} with somewhat undefined symbol;
2015-11-07, by wenzelm
ML cartouches via control antiquotation;
2015-11-07, by wenzelm
more formal treatment of control symbols;
2015-11-06, by wenzelm
more antiquotations;
2015-11-06, by wenzelm
more antiquotations;
2015-11-06, by wenzelm
retain traditional rendering of \<paragraph>;
2015-11-06, by wenzelm
added glyphs 0x204b, 0x2b1a from DejaVuSansMono;
2015-11-06, by wenzelm
tuned;
2015-11-06, by wenzelm
tuned
2015-11-06, by nipkow
tuned
2015-11-05, by nipkow
updating options to verit
2015-11-05, by fleury
isabelle update_cartouches -c -t;
2015-11-05, by wenzelm
isabelle update_cartouches -c -t;
2015-11-05, by wenzelm
IsabelleText for unusual symbol;
2015-11-05, by wenzelm
isabelle update_cartouches -c;
2015-11-05, by wenzelm
merged
2015-11-05, by nipkow
Convertd to 3-way comparisons
2015-11-05, by nipkow
isabelle update_cartouches -c;
2015-11-05, by wenzelm
symbolic syntax "\<comment> text";
2015-11-05, by wenzelm
avoid ligatures;
2015-11-04, by wenzelm
added propertional dashes from DejaVuSans (not Mono): 0x2013, 0x2014, 0x2015;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
updated;
2015-11-04, by wenzelm
more antiquotations;
2015-11-04, by wenzelm
document antiquotation @{footnote};
2015-11-04, by wenzelm
dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
2015-11-04, by wenzelm
eliminated Nitpick's pedantic support for 'emdash'
2015-11-04, by blanchet
tuned;
2015-11-04, by wenzelm
NEWS;
2015-11-04, by wenzelm
Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04, by ballarin
Qualifiers in locale expressions default to mandatory regardless of the command.
2015-11-04, by ballarin
merged
2015-11-03, by wenzelm
tuned signature;
2015-11-03, by wenzelm
prefer Isabelle/Scala Future;
2015-11-03, by wenzelm
prefer Isabelle/Scala Future;
2015-11-03, by wenzelm
tuned imports;
2015-11-03, by wenzelm
more direct task future implementation, with proper cancel operation;
2015-11-03, by wenzelm
tuned;
2015-11-03, by wenzelm
prefer ad-hoc non-worker threads;
2015-11-03, by wenzelm
clarified modules;
2015-11-03, by wenzelm
cancel already running request;
2015-11-03, by wenzelm
added acknowledgement in Binomial.thy
2015-11-03, by eberlm
Merged
2015-11-03, by eberlm
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02, by eberlm
don't pollute local theory with needless names
2015-11-02, by blanchet
allow selectors and discriminators with same name as type
2015-11-02, by blanchet
make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
2015-11-02, by blanchet
merged
2015-11-02, by wenzelm
avoid premature flushing and thus flashing of text area;
2015-11-02, by wenzelm
tuned whitespace;
2015-11-02, by wenzelm
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
2015-11-02, by wenzelm
redundant;
2015-11-02, by wenzelm
tuned whitespace;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
isabelle update_cartouches -t;
2015-11-02, by wenzelm
avoid highlighted area getting "stuck" after edit;
2015-11-02, by wenzelm
clarified completion of Isabelle symbols within document source;
2015-11-02, by wenzelm
more accurate imports: allow re-uses of base names in PIDE interaction (amending 60c159d490a2);
2015-11-02, by wenzelm
merged
2015-11-02, by nipkow
tuned names and optimized comparison order
2015-11-02, by nipkow
updated CVC4 component to deal with paths with whitespace
2015-11-02, by blanchet
Merged
2015-11-02, by eberlm
Rounding function, uniform limits, cotangent, binomial identities
2015-11-02, by eberlm
merged
2015-10-31, by wenzelm
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
2015-10-31, by wenzelm
global start time as reference point;
2015-10-31, by wenzelm
tuned signature -- clarified modules;
2015-10-30, by wenzelm
obsolete (see 9c6346319eee, 7924d61b50cf);
2015-10-30, by wenzelm
added splay trees
2015-10-30, by nipkow
added many small lemmas about setsum/setprod/powr/...
2015-10-29, by eberlm
no icons here -- not a standalone window;
2015-10-27, by wenzelm
workaround for problem with C-1, C-2, C-3 seen on Slovak QWERTY keyboard;
2015-10-27, by wenzelm
removed presumably obsolete workaround (see 7924d61b50cf);
2015-10-27, by wenzelm
Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-27, by paulson
merged
2015-10-26, by paulson
new lemmas about topology, etc., for Cauchy integral formula
2015-10-26, by paulson
adapted to 436b7fe89cdc
2015-10-26, by nipkow
clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
2015-10-26, by wenzelm
added 234-trees (slow)
2015-10-25, by nipkow
added 234-Trees (slow)
2015-10-25, by nipkow
tuned
2015-10-25, by nipkow
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
2015-10-24, by wenzelm
updated to jedit-5.3.0 and SideKick 1.8;
2015-10-23, by wenzelm
updated to jdk-8u66;
2015-10-23, by wenzelm
print thm wrt. local shyps (from full proof context);
2015-10-23, by wenzelm
clarified modules;
2015-10-23, by wenzelm
proper transfer of stored facts;
2015-10-23, by wenzelm
tuned;
2015-10-22, by wenzelm
more robust ASCII output: avoid ligatures of quotes;
2015-10-22, by wenzelm
tuned;
2015-10-22, by wenzelm
more control symbols;
2015-10-22, by wenzelm
clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;
2015-10-22, by wenzelm
rendering for \<^verbatim>;
2015-10-21, by wenzelm
Isabelle fonts via external component;
2015-10-21, by wenzelm
tuned document;
2015-10-21, by wenzelm
tuned document;
2015-10-21, by wenzelm
added glyphs 0x25a9 from DejaVuSansMono;
2015-10-21, by wenzelm
removed generated files from repository;
2015-10-21, by wenzelm
tuned;
2015-10-21, by wenzelm
proper spaces around @{text};
2015-10-21, by wenzelm
isabelle update_cartouches -t;
2015-10-20, by wenzelm
added isabelle update_cartouches option -t;
2015-10-20, by wenzelm
another antiquotation short form: undecorated cartouche as alias for @{text};
2015-10-20, by wenzelm
repaired document;
2015-10-19, by wenzelm
more symbols;
2015-10-19, by wenzelm
tuned English;
2015-10-19, by wenzelm
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
2015-10-19, by wenzelm
tuned document;
2015-10-19, by wenzelm
merged
2015-10-19, by wenzelm
avoid odd permissions of fresh tmp_file;
2015-10-19, by wenzelm
added action "isabelle-emph";
2015-10-19, by wenzelm
tuned;
2015-10-19, by wenzelm
tuned;
2015-10-19, by wenzelm
tuned text
2015-10-19, by nipkow
tuned;
2015-10-18, by wenzelm
merged
2015-10-18, by wenzelm
more control symbols;
2015-10-18, by wenzelm
tuned signature;
2015-10-18, by wenzelm
tuned signature;
2015-10-18, by wenzelm
clarified;
2015-10-18, by wenzelm
clarified control antiquotations: decode control symbol to get name;
2015-10-18, by wenzelm
more documentation;
2015-10-18, by wenzelm
support control symbol antiquotations;
2015-10-18, by wenzelm
clarified Symbol.is_control;
2015-10-18, by wenzelm
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
2015-10-18, by nipkow
code abbreviation for mapping over a fixed range
2015-10-17, by haftmann
back to lxbroy3, which appears to be free at the moment;
2015-10-17, by wenzelm
tuned signature;
2015-10-17, by wenzelm
merged
2015-10-17, by wenzelm
more uniform command setup;
2015-10-17, by wenzelm
added 'paragraph', 'subparagraph';
2015-10-17, by wenzelm
clarified Latex.environment;
2015-10-17, by wenzelm
more explicit output of list items;
2015-10-17, by wenzelm
tuned;
2015-10-17, by wenzelm
clarified nesting of paragraphs: indentation is taken into account more uniformly;
2015-10-17, by wenzelm
Markdown support in document text;
2015-10-16, by wenzelm
clarified Antiquote.antiq_reports;
2015-10-16, by wenzelm
trim_blanks after read, before eval;
2015-10-15, by wenzelm
clarified modules;
2015-10-15, by wenzelm
load markdown.ML into Pure;
2015-10-15, by wenzelm
proper recursive nesting of adjacent lists;
2015-10-15, by wenzelm
tuned;
2015-10-15, by wenzelm
clarified line content: source without marker prefix;
2015-10-15, by wenzelm
more markup;
2015-10-15, by wenzelm
report Markdown document structure;
2015-10-15, by wenzelm
more comments;
2015-10-15, by wenzelm
unused -- avoid confusion in Symbols dockable;
2015-10-15, by wenzelm
proper nesting of adjacent lists;
2015-10-15, by wenzelm
more document structure;
2015-10-15, by wenzelm
more document structure;
2015-10-14, by wenzelm
more document structure;
2015-10-14, by wenzelm
clarified;
2015-10-14, by wenzelm
minimal support for Markdown documents;
2015-10-14, by wenzelm
clarified;
2015-10-14, by wenzelm
less
more
|
(0)
-30000
-10000
-1920
+1920
+10000
tip