isabelle: Graph

added Haskabelle -- in accordance to website/index.html version f397b96e3ad2;
2009-04-14, by wenzelm
ISABELLE_USEDIR_OPTIONS: less ambitious -M1 by default -- multithreading is largely untested on fringe platforms (cygwin, solaris);
2009-04-14, by wenzelm
misc updates for Isabelle2009;
2009-04-14, by wenzelm
Added tag isa2009-test for changeset dda08b76fa99
2009-04-08, by wenzelm
updated official title of contribution by Johannes Hoelzl;
2009-04-08, by wenzelm
misc tuning and updates;
2009-04-07, by wenzelm
updated doc setup;
2009-04-07, by wenzelm
merged
2009-04-07, by wenzelm
moved generated eps/pdf to main directory, for proper display in dvi;
2009-04-07, by wenzelm
updates for E-1.0-004;
2009-04-07, by wenzelm
tuned manual
2009-04-07, by haftmann
merged
2009-04-06, by haftmann
tuned comment
2009-04-06, by haftmann
Added tag isa2009-test for changeset 613c2eb8aef6
2009-04-06, by wenzelm
tuned whitespace
2009-04-06, by haftmann
merged
2009-04-05, by wenzelm
reverted to explicitly check the presence of a refutation
2009-04-04, by immler
tuned white space;
2009-04-05, by wenzelm
merged
2009-04-05, by wenzelm
\nolinkurl for dvi mode recovers hyphenation of URLs -- this already works by default in PDF mode;
2009-04-05, by wenzelm
removed obsolete website directory -- information derived by website/build;
2009-04-05, by wenzelm
More precise treatement of rational constants by the normalizer for fields
2009-04-05, by chaieb
fixed usage of rational constants
2009-04-05, by chaieb
No Complex_Main needed
2009-04-05, by chaieb
now deals with devision in fields
2009-04-05, by chaieb
fixed formal markup;
2009-04-03, by wenzelm
merged
2009-04-03, by nipkow
Finite_Set: lemma
2009-04-03, by nipkow
single-threaded build;
2009-04-03, by wenzelm
merged
2009-04-03, by berghofe
Added check whether argument types of inductive set agree with types of declared
2009-04-03, by berghofe
added setsum_eq_1_iff
2009-04-03, by nipkow
simplified website/config;
2009-04-02, by wenzelm
Updated to corrected E output messages
2009-04-02, by nipkow
updated keywords (with polyml-experimental);
2009-04-02, by wenzelm
some more HOL-Nominal news;
2009-04-02, by wenzelm
merged
2009-04-02, by wenzelm
tuned signature;
2009-04-02, by wenzelm
misc tuning for release;
2009-04-02, by wenzelm
merged
2009-04-02, by berghofe
Fixed bug in transformation of congruence rule for ==
2009-04-02, by berghofe
some HOL-Nominal news;
2009-04-02, by wenzelm
updates for Isabelle2009 release;
2009-04-02, by wenzelm
tuned;
2009-04-02, by wenzelm
merged
2009-04-02, by wenzelm
misc cleanup and rearrangements for Isabelle2009 release;
2009-04-02, by wenzelm
merged
2009-04-01, by nipkow
cleaned up setprod_zero-related lemmas
2009-04-01, by nipkow
merged
2009-04-01, by huffman
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
2009-04-01, by huffman
added nat_div_gt_0 [simp]
2009-04-01, by nipkow
added setsum_pos_nat
2009-04-01, by nipkow
merged
2009-04-01, by nipkow
added strong_setprod_cong[cong] (in analogy with setsum)
2009-04-01, by nipkow
proper external tikz pictures
2009-04-01, by haftmann
merged
2009-04-01, by wenzelm
tuned comments;
2009-04-01, by wenzelm
merged
2009-04-01, by wenzelm
explicitly check that at least one argument is present to avoid low-level exception
2009-04-01, by krauss
merged
2009-04-01, by wenzelm
included managing_thread in state of AtpManager:
2009-03-31, by immler
domain package registers induction rules
2009-03-31, by huffman
merged
2009-03-31, by wenzelm
Merged.
2009-03-31, by ballarin
Improvements to the text.
2009-03-31, by ballarin
fixed header;
2009-03-31, by wenzelm
fixed header;
2009-03-31, by wenzelm
added dest_conjunctions (cf. Logic.dest_conjunctions);
2009-03-31, by wenzelm
superficial tuning;
2009-03-31, by wenzelm
merged
2009-03-31, by wenzelm
merged
2009-03-31, by wenzelm
schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
2009-03-31, by wenzelm
updated latex requirement;
2009-03-31, by wenzelm
tuned document;
2009-03-31, by wenzelm
replaced 'a set by abstract 'a::complete_lattice, and recover plain reasoning instead of adhoc automation (by simp);
2009-03-31, by wenzelm
tuned error message;
2009-03-31, by wenzelm
tuned;
2009-03-31, by wenzelm
suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;
2009-03-31, by wenzelm
generalized pull to anamorph
2009-03-31, by haftmann
merged
2009-03-31, by haftmann
ML snippets for experimental evaluation
2009-03-31, by haftmann
merged
2009-03-30, by wenzelm
merged
2009-03-30, by huffman
domain package declares more simp rules
2009-03-30, by huffman
simplified 'print_orders' command;
2009-03-30, by wenzelm
tuned;
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
simplify theorem references
2009-03-30, by huffman
added Toplevel.previous_node_of;
2009-03-30, by wenzelm
tuned spacing and formatting;
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
terminate watching thread
2009-03-30, by immler
merged
2009-03-30, by wenzelm
no longer delay loading of assoc_fold.ML
2009-03-30, by huffman
qualified_name_of: observe empty case;
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
merged
2009-03-30, by huffman
add more lemmas for signed comparisons
2009-03-27, by huffman
use standard parsers provided by SpecParse
2009-03-30, by krauss
bstring -> binding
2009-03-30, by krauss
code attribute for tailrec-equations, too; tuned
2009-03-30, by krauss
optimistically add code attribute to .simps without further checks
2009-03-30, by krauss
remove "otherwise" feature from function package which was never really documented or used
2009-03-30, by krauss
prep_full_context_statement: explicit record of flags;
2009-03-30, by wenzelm
Limit the number of results returned by auto_solves.
2009-03-30, by Timothy Bourke
merged
2009-03-29, by wenzelm
Merged.
2009-03-29, by ballarin
In interpretation: equations are not propagated through the hierarchy automatically.
2009-03-29, by ballarin
Normalise equation only for morphism, not thm stored in theory.
2009-03-29, by ballarin
Default mode of qualifiers in locale commands.
2009-03-28, by ballarin
Front matter updated.
2009-03-28, by ballarin
tuned;
2009-03-29, by wenzelm
simplified Element.activate(_i): singleton version;
2009-03-29, by wenzelm
tuned;
2009-03-29, by wenzelm
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
2009-03-29, by wenzelm
unified binding prefix terminology;
2009-03-29, by wenzelm
simplified roundup activation interface;
2009-03-29, by wenzelm
merged
2009-03-28, by wenzelm
merged
2009-03-28, by haftmann
merged
2009-03-28, by haftmann
second attempt for code_deps command
2009-03-28, by haftmann
merged
2009-03-28, by haftmann
corrected projection of required statement names
2009-03-28, by haftmann
corrected check for additional type variables on rhs of code equations
2009-03-28, by haftmann
not yet fruitful tex experiments with bounding boxes
2009-03-28, by haftmann
simplified Locale.activate operations, using generic context;
2009-03-28, by wenzelm
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28, by wenzelm
define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
2009-03-28, by wenzelm
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28, by wenzelm
simplified references to facts, eliminated external note_thmss;
2009-03-28, by wenzelm
added map_facts_refs;
2009-03-28, by wenzelm
tuned;
2009-03-28, by wenzelm
replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-28, by wenzelm
replaced add_binds by singleton bind_term;
2009-03-28, by wenzelm
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-28, by wenzelm
minor tuning;
2009-03-28, by wenzelm
merged
2009-03-28, by wenzelm
Merged.
2009-03-28, by ballarin
Corrections to locale syntax.
2009-03-28, by ballarin
Update explanation of locale expressions to locale reimplementation.
2009-03-27, by ballarin
Comments updated.
2009-03-27, by ballarin
fixed proof
2009-03-27, by chaieb
merged
2009-03-27, by chaieb
fps made instance of number_ring
2009-03-27, by chaieb
updated keywords with polyml-experimental;
2009-03-27, by wenzelm
export position_of;
2009-03-27, by wenzelm
dropped infix union
2009-03-27, by haftmann
tuned notoriously slow metis proof
2009-03-27, by haftmann
merged
2009-03-27, by haftmann
dropped toy example Code_Antiq
2009-03-27, by haftmann
more convenient name uniqueness
2009-03-27, by haftmann
normalized imports
2009-03-27, by haftmann
dropped legacy goal package call
2009-03-27, by haftmann
merged
2009-03-27, by haftmann
merged
2009-03-26, by haftmann
step towards proper pictures in dvi
2009-03-26, by haftmann
merged
2009-03-26, by wenzelm
parameterize assoc_fold with is_numeral predicate
2009-03-26, by huffman
merged
2009-03-26, by paulson
New theorems mostly concerning infinite series.
2009-03-26, by paulson
interpretation/interpret: prefixes are mandatory by default;
2009-03-26, by wenzelm
interpretation/interpret: prefixes are mandatory by default;
2009-03-26, by wenzelm
interpretation/interpret: prefixes within locale expression are mandatory by default;
2009-03-26, by wenzelm
locale_expression: mandatory as parameter;
2009-03-26, by wenzelm
register_locale: produce stamps at the spot where elements are registered;
2009-03-26, by wenzelm
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
2009-03-26, by wenzelm
pretty_thm_aux etc.: explicit show_status flag;
2009-03-26, by wenzelm
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-26, by wenzelm
@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
2009-03-25, by wenzelm
tuned;
2009-03-25, by wenzelm
use more informative Thm.proof_body_of for oracle demo;
2009-03-25, by wenzelm
Proofterm.approximate_proof_body;
2009-03-25, by wenzelm
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
2009-03-25, by wenzelm
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
2009-03-25, by wenzelm
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;
2009-03-25, by wenzelm
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
2009-03-24, by wenzelm
status_of: need to include local promises as well!
2009-03-24, by wenzelm
status_of: simultaneous list;
2009-03-24, by wenzelm
display derivation status of thms;
2009-03-24, by wenzelm
recover old ids;
2009-03-24, by wenzelm
report ML typing;
2009-03-24, by wenzelm
merged
2009-03-24, by wenzelm
merged
2009-03-24, by nipkow
NEWS: [arith]
2009-03-24, by nipkow
get_index: produce index of next pending token, not the last one;
2009-03-24, by wenzelm
register token positions persistently with context;
2009-03-24, by wenzelm
tuned;
2009-03-24, by wenzelm
more markup elements for ML programs;
2009-03-24, by wenzelm
merged
2009-03-24, by wenzelm
process at-sml-dev last -- takes very long (why?);
2009-03-24, by wenzelm
fix
2009-03-24, by nipkow
merged
2009-03-24, by nipkow
presburger uses [arith] now
2009-03-24, by nipkow
merged
2009-03-24, by wenzelm
merged
2009-03-24, by haftmann
added Imperative_HOL_ex
2009-03-24, by haftmann
Use assms rather than prems in find_theorems solves.
2009-03-24, by Timothy Bourke
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
2009-03-23, by huffman
lemmas add_sign_intros
2009-03-23, by huffman
merged
2009-03-23, by haftmann
moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-23, by haftmann
corrected variable renaming
2009-03-23, by haftmann
tuned error messages
2009-03-23, by haftmann
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-23, by haftmann
structure LinArith now named Lin_Arith
2009-03-23, by haftmann
suddenly infix identifier oo occurs in generated code
2009-03-23, by haftmann
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-24, by wenzelm
eliminated non-canonical alias structure T = ML_Lex;
2009-03-24, by wenzelm
error "Static Errors";
2009-03-24, by wenzelm
more systematic type use_context;
2009-03-24, by wenzelm
tuned;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
eliminated Output.ml_output;
2009-03-23, by wenzelm
pretty_ml/ml_pretty: proper handling of markup and string length;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
removed obsolete ml_output;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-23, by wenzelm
de-camelized ML_Name_Space;
2009-03-23, by wenzelm
suppress status output for traditional tty modes (including Proof General);
2009-03-23, by wenzelm
added report_text -- status messages with text body;
2009-03-23, by wenzelm
maintain parse trees cumulatively;
2009-03-23, by wenzelm
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
2009-03-23, by wenzelm