| 2013-11-18 |
traytel |
show all involved subtyping constraints that cause coercion inference to fail
|
changeset |
files
|
| 2013-11-18 |
hoelzl |
additional lemmas in BNF/Examples/Stream
|
changeset |
files
|
| 2013-11-18 |
traytel |
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
|
changeset |
files
|
| 2013-11-18 |
nipkow |
comments by Sean Seefried
|
changeset |
files
|
| 2013-11-17 |
wenzelm |
more robust example;
|
changeset |
files
|
| 2013-11-17 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-11-17 |
wenzelm |
tuned;
|
changeset |
files
|
| 2013-11-17 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-11-17 |
wenzelm |
explicit indication of thy_load commands;
|
changeset |
files
|
| 2013-11-17 |
wenzelm |
centralized management of pending buffer edits;
|
changeset |
files
|
| 2013-11-17 |
nipkow |
merged
|
changeset |
files
|
| 2013-11-16 |
nipkow |
added functions all and exists to IArray
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
prefer explicit "document" flag -- eliminated stateful Present.no_document;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
simplified HTML linefeed (again, see 041dc6d8d344);
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
simplified HTML theory presentation;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
tuned;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
merged
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
tuned signature -- clarified Proof General legacy;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
toplevel function "use" refers to raw ML bootstrap environment;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
obsolete;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
updated example;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
prefer UTF8.decode_permissive;
|
changeset |
files
|
| 2013-11-16 |
wenzelm |
more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;
|
changeset |
files
|
| 2013-11-15 |
wenzelm |
more specific Protocol_Output: empty message.body, main content via bytes/text;
|
changeset |
files
|
| 2013-11-14 |
wenzelm |
tuned imports;
|
changeset |
files
|
| 2013-11-14 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2013-11-14 |
wenzelm |
immutable byte vectors versus UTF8 strings;
|
changeset |
files
|
| 2013-11-15 |
haftmann |
dropped duplicate of of_bool
|
changeset |
files
|
| 2013-11-15 |
haftmann |
proper code equations for Gcd and Lcm on nat and int
|
changeset |
files
|
| 2013-11-16 |
nipkow |
tuned
|
changeset |
files
|
| 2013-11-14 |
blanchet |
fixed type variable confusion in 'datatype_new_compat'
|
changeset |
files
|
| 2013-11-14 |
blanchet |
implemented 'tptp_translate'
|
changeset |
files
|
| 2013-11-14 |
blanchet |
reintroduced (unimplemented) 'tptp_translate' tool
|
changeset |
files
|
| 2013-11-14 |
blanchet |
have MaSh support nameless facts (i.e. proofs) and use that support
|
changeset |
files
|
| 2013-11-14 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| 2013-11-14 |
blanchet |
renamed thm
|
changeset |
files
|
| 2013-11-14 |
haftmann |
explicit inclusion of data refinement theory into HOL-Library session
|
changeset |
files
|
| 2013-11-14 |
nipkow |
tuned to improve automation (for REPEAT)
|
changeset |
files
|
| 2013-11-13 |
haftmann |
separated comparision on bit operations into separate theory
|
changeset |
files
|
| 2013-11-13 |
traytel |
prohibit locally fixed type variables in bnf definitions
|
changeset |
files
|
| 2013-11-13 |
traytel |
tuned
|
changeset |
files
|
| 2013-11-13 |
traytel |
standard relator for list bnf
|
changeset |
files
|
| 2013-11-13 |
traytel |
tuned example
|
changeset |
files
|
| 2013-11-13 |
blanchet |
shortened generated property name
|
changeset |
files
|
| 2013-11-13 |
traytel |
more explicit syntax for defining a bnf
|
changeset |
files
|
| 2013-11-13 |
hoelzl |
fix document generation for HOL-Probability
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
fix document generation for Extended_Nat
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
measure of a countable union
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
add restrict_space measure
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
better support for enat and ereal conversions
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
enat is countable
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
add equalities for SUP and INF over constant functions
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
add acyclicI_order
|
changeset |
files
|
| 2013-11-12 |
hoelzl |
stronger inc_induct and dec_induct
|
changeset |
files
|