isabelle: Graph

pat_completeness gets its own file
2009-10-23, by krauss
ignore error messages produced by ATPs
2009-10-23, by boehmes
merged
2009-10-23, by haftmann
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)
2009-10-23, by haftmann
restored accidentally deleted submultiset
2009-10-22, by haftmann
multiset operations with canonical argument order
2009-10-22, by haftmann
arg_types_of auxiliary function; using multiset operations
2009-10-22, by haftmann
merged
2009-10-23, by haftmann
close thm derivations explicitly
2009-10-22, by haftmann
Fix a duplicate abbreviation || in etc/symbols.
2009-10-23, by tbourke
made SML/NJ happy;
2009-10-22, by wenzelm
updated session name;
2009-10-22, by wenzelm
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
2009-10-22, by wenzelm
merged
2009-10-22, by wenzelm
merged
2009-10-22, by wenzelm
merged
2009-10-21, by wenzelm
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
2009-10-21, by wenzelm
merged
2009-10-22, by wenzelm
explicit close_derivation
2009-10-22, by haftmann
merged
2009-10-22, by haftmann
map_range (and map_index) combinator
2009-10-22, by haftmann
dropped Datatype.distinct_simproc
2009-10-22, by haftmann
use Synchronized.assign to achieve actual immutable results;
2009-10-22, by wenzelm
support single-assigment variables -- based on magic RTS operations by David Matthews;
2009-10-22, by wenzelm
merged
2009-10-22, by boehmes
fixed permissions -- this is a script, not an executable
2009-10-22, by boehmes
inv_onto -> inv_into
2009-10-22, by nipkow
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-21, by blanchet
merged
2009-10-21, by blanchet
fixed the "expect" mechanism of Refute in the face of timeouts
2009-10-21, by blanchet
removed "nitpick_const_simp" attribute from Record's "simps";
2009-10-21, by blanchet
merged
2009-10-21, by haftmann
more accurate removal
2009-10-21, by haftmann
merged
2009-10-21, by haftmann
curried inter as canonical list operation (beware of argument order)
2009-10-21, by haftmann
merged
2009-10-21, by boehmes
proper handling of single literal case,
2009-10-21, by boehmes
Removed the hard-wired white list of theorems for sledgehammer
2009-10-21, by paulson
merged
2009-10-21, by paulson
Some new lemmas concerning sets
2009-10-20, by paulson
merged
2009-10-21, by haftmann
curried union as canonical list operation
2009-10-21, by haftmann
tuned ML import
2009-10-21, by haftmann
removed old-style \ and \\ infixes
2009-10-21, by haftmann
merged
2009-10-21, by haftmann
dropped redundant gen_ prefix
2009-10-21, by haftmann
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20, by haftmann
find_theorems: better handling of abbreviations (by Timothy Bourke)
2009-10-21, by kleing
standardized basic operations on type option;
2009-10-21, by wenzelm
eliminated THENL -- use THEN RANGE;
2009-10-20, by wenzelm
tuned;
2009-10-20, by wenzelm
fixed SML/NJ toplevel pp;
2009-10-20, by wenzelm
backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-20, by wenzelm
tuned;
2009-10-20, by wenzelm
uniform use of Integer.min/max;
2009-10-20, by wenzelm
modernized session SET_Protocol;
2009-10-20, by wenzelm
modernized session Metis_Examples;
2009-10-20, by wenzelm
modernized session Isar_Examples;
2009-10-20, by wenzelm
tuned header;
2009-10-20, by wenzelm
more accurate dependencies for HOL-SMT, which is a session with image;
2009-10-20, by wenzelm
removed unused map_force;
2009-10-20, by wenzelm
Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-20, by paulson
additional schematic rules for Z3's rewrite rule
2009-10-20, by boehmes
merged
2009-10-20, by nipkow
added Hilbert_Choice section
2009-10-20, by nipkow
merged
2009-10-20, by boehmes
eliminated extraneous wrapping of public records,
2009-10-20, by boehmes
proper exceptions instead of unhandled partiality
2009-10-20, by boehmes
footnote: inv via inv_onto
2009-10-20, by nipkow
added inv_def for compatibility as a lemma
2009-10-20, by nipkow
slightly less context-sensitive settings;
2009-10-20, by wenzelm
merged
2009-10-20, by wenzelm
corrected paths to certificates,
2009-10-20, by boehmes
added proof reconstructon for Z3,
2009-10-20, by boehmes
merged
2009-10-20, by wenzelm
merged
2009-10-20, by haftmann
more accurate checkpoints
2009-10-20, by haftmann
dropped lazy code equations
2009-10-19, by haftmann
CONTRIBUTORS
2009-10-19, by haftmann
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-19, by wenzelm
eliminated duplicate fold1 -- beware of argument order!
2009-10-19, by wenzelm
uniform use of Integer.add/mult/sum/prod;
2009-10-19, by wenzelm
Removed dead code in function mk_deftab.
2009-10-19, by berghofe
Removed unneeded reference to inv_def.
2009-10-19, by berghofe
Replaced inv by the_inv_onto.
2009-10-19, by berghofe
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
2009-10-19, by berghofe
fixed proof (cf. d1d4d7a08a66);
2009-10-18, by wenzelm
removed disjunctive group cancellation -- provers run independently;
2009-10-18, by wenzelm
tuned;
2009-10-18, by wenzelm
removed some unreferenced material;
2009-10-18, by wenzelm
merged
2009-10-18, by nipkow
certificates for sos
2009-10-18, by nipkow
merged
2009-10-18, by nipkow
added sums of squares for standard deviation
2009-10-18, by nipkow
merged
2009-10-18, by nipkow
Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-18, by nipkow
disable indent-tabs-mode in Proof General / Emacs;
2009-10-18, by wenzelm
merged
2009-10-17, by wenzelm
made SML/NJ happy;
2009-10-17, by wenzelm
Merged.
2009-10-17, by ballarin
Finished revisions of locales tutorial.
2009-10-17, by ballarin
Changed part of the examples to int.
2009-10-15, by ballarin
Save current state of locales tutorial.
2009-10-15, by ballarin
Observe order of declaration when printing registrations.
2009-10-15, by ballarin
disable sunbroy2 for now;
2009-10-17, by wenzelm
tuned/moved divide_and_conquer';
2009-10-17, by wenzelm
tuned;
2009-10-17, by wenzelm
removed separate record_quick_and_dirty_sensitive;
2009-10-17, by wenzelm
simplified tactics;
2009-10-17, by wenzelm
eliminated old List.foldr and OldTerm operations;
2009-10-17, by wenzelm
removed unused names;
2009-10-17, by wenzelm
misc tuning and simplification;
2009-10-17, by wenzelm
less pervasive names;
2009-10-17, by wenzelm
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17, by wenzelm
Method.cheating: check quick_and_dirty here;
2009-10-17, by wenzelm
tuned;
2009-10-17, by wenzelm
Unsynchronized.set etc.;
2009-10-17, by wenzelm
indicate CRITICAL nature of various setmp combinators;
2009-10-17, by wenzelm
ISABELLE_TOOL;
2009-10-17, by wenzelm
tuned signature;
2009-10-17, by wenzelm
merged
2009-10-17, by wenzelm
merged
2009-10-17, by nipkow
added the_inv_onto
2009-10-17, by nipkow
eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-17, by wenzelm
removed obsolete old goal command;
2009-10-17, by wenzelm
legacy Drule.standard is no longer pervasive;
2009-10-17, by wenzelm
explicitly qualify Drule.standard;
2009-10-17, by wenzelm
tuned white space;
2009-10-16, by wenzelm
local channels for tracing/debugging;
2009-10-16, by wenzelm
made SML/NJ happy;
2009-10-16, by wenzelm
sunbroy2: back to single-threaded mode for now -- deadlock in Poly/ML 5.3-SVN-900;
2009-10-15, by wenzelm
replaced String.concat by implode;
2009-10-15, by wenzelm
space_implode;
2009-10-15, by wenzelm
normalized aliases of Output operations;
2009-10-15, by wenzelm
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
2009-10-15, by wenzelm
natural argument order for prover;
2009-10-15, by wenzelm
ATP_Manager.get_prover: canonical argument order;
2009-10-15, by wenzelm
tuned proof (via atp_minimized);
2009-10-15, by wenzelm
sort_strings (cf. Pure/library.ML);
2009-10-15, by wenzelm
clarified File.platform_path vs. File.shell_path;
2009-10-15, by wenzelm
exported File.shell_quote;
2009-10-15, by wenzelm
misc tuning and recovery of Isabelle coding style;
2009-10-15, by wenzelm
eliminated extraneous wrapping of public records;
2009-10-15, by wenzelm
tuned signature;
2009-10-15, by wenzelm
renamed functor HeapFun to Heap;
2009-10-15, by wenzelm
misc tuning and clarification;
2009-10-15, by wenzelm
structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
2009-10-15, by wenzelm
modernized structure names;
2009-10-14, by wenzelm
show direct GC time (which is included in CPU time);
2009-10-14, by wenzelm
eliminated obsolete C/flip combinator;
2009-10-14, by wenzelm
added List.nth
2009-10-14, by nipkow
tuned make parameters for sunbroy2;
2009-10-14, by wenzelm
accomodate old version of "tail", e.g. on sunbroy2;
2009-10-14, by wenzelm
settings for parallel experimental Poly/ML 5.3;
2009-10-14, by wenzelm
sharpened name
2009-10-14, by haftmann
more explicit notion of canonized code equations
2009-10-14, by haftmann
more explicit notion of canonized code equations
2009-10-14, by haftmann
tuned whitespace
2009-10-14, by haftmann
tuned whitespace
2009-10-14, by haftmann
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
2009-10-14, by haftmann
merged
2009-10-13, by haftmann
deactivated Datatype.distinct_simproc
2009-10-13, by haftmann
dropped Datatype.distinct_simproc; tuned
2009-10-13, by haftmann
order conjunctions to be printed without parentheses
2009-10-13, by hoelzl
approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
2009-10-13, by hoelzl
merged
2009-10-13, by haftmann
added add_tyconames; tuned
2009-10-12, by haftmann
merged
2009-10-13, by haftmann
more appropriate abstraction over distinctness rules
2009-10-13, by haftmann
merged
2009-10-12, by haftmann
intro_base_names combinator
2009-10-12, by haftmann
merged
2009-10-12, by haftmann
dropped dist_ss
2009-10-12, by haftmann
merged
2009-10-12, by haftmann
added is_IVar
2009-10-12, by haftmann
factored out Code_Printer.aux_params
2009-10-12, by haftmann
dropped rule duplicates
2009-10-12, by haftmann
less non-standard combinators
2009-10-12, by haftmann
nth replaces List.nth
2009-10-12, by haftmann
dropped redundancy
2009-10-12, by haftmann
dropped dead code
2009-10-12, by haftmann
using distinct rules directly
2009-10-12, by haftmann
simplified proof
2009-10-09, by haftmann
dropped simproc_dist formally
2009-10-09, by haftmann
tuned order of lemmas
2009-10-09, by haftmann
term styles also cover antiquotations term_type and typeof
2009-10-09, by haftmann
merged
2009-10-09, by haftmann
lookup for datatype constructors considers type annotations to resolve overloading
2009-10-08, by haftmann
added group_stmts
2009-10-08, by haftmann
moved labelled_name to code_thingol
2009-10-08, by haftmann
updated generated documentation
2009-10-08, by haftmann
corrected syntax diagrams for styles
2009-10-08, by haftmann
new generalized concept for term styles
2009-10-08, by haftmann
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
2009-10-07, by haftmann
isatest: store test identifiers
2009-10-08, by krauss
tuned proofs
2009-10-07, by haftmann
added bot_boolE, top_boolI
2009-10-07, by haftmann
do not use Locale.add_registration_eqs any longer
2009-10-07, by haftmann
Inf/Sup now purely syntactic
2009-10-07, by haftmann
merged
2009-10-06, by haftmann
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-10-06, by haftmann
merged
2009-10-06, by haftmann
added Coset as constructor
2009-10-06, by haftmann
sets and cosets
2009-10-06, by haftmann
added syntactic Inf and Sup
2009-10-06, by haftmann
merged
2009-10-05, by paulson
New lemmas connected with the reals and infinite series
2009-10-05, by paulson
New facts about domain and range in
2009-10-05, by paulson
merged
2009-10-05, by haftmann
experimental de-facto abolishment of distinctness limit
2009-10-05, by haftmann
tuned handling of type variable names further
2009-10-05, by haftmann
variables in type schemes must be renamed simultaneously with variables in equations
2009-10-05, by haftmann
explicitly unsynchronized
2009-10-05, by haftmann
explicitly unsynchronized
2009-10-05, by haftmann
recovered support for Spass: re-enabled writing problems in DFG format
2009-10-04, by boehmes
avoid exception Option: only apply "the" if needed
2009-10-04, by boehmes
merged
2009-10-04, by nipkow
atp_minimal using chain_ths again
2009-09-30, by Philipp Meyer
merged
2009-10-03, by boehmes
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
2009-10-03, by boehmes
eliminated dead code;
2009-10-02, by wenzelm
eliminated dead code and redundant parameters;
2009-10-02, by wenzelm
eliminated dead code;
2009-10-02, by wenzelm
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02, by wenzelm
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02, by wenzelm
Refute.refute_goal: goal addressing from 1 as usual;
2009-10-02, by wenzelm
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
2009-10-02, by wenzelm
clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-10-02, by wenzelm
misc tuning and simplification;
2009-10-02, by wenzelm
macbroy2: bigger jobs first, to avoid danger of swapping during daytime;
2009-10-02, by wenzelm
less ambitious heap settings;
2009-10-02, by wenzelm
merged
2009-10-02, by haftmann
merged
2009-10-01, by haftmann
proper merge of interpretation equations
2009-10-01, by haftmann
merged
2009-10-02, by wenzelm
Merged again.
2009-10-01, by ballarin
Merged.
2009-10-01, by ballarin
News entry: inheritance of mixins; print_interps.
2009-10-01, by ballarin
Avoid administrative overhead for identity mixins.
2009-10-01, by ballarin
tuned;
2009-10-01, by wenzelm