Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+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.
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
tip