isabelle: Graph

merged
2009-07-20, by haftmann
less digestible
2009-07-20, by haftmann
refined outline structure
2009-07-20, by haftmann
replaced usedir option -Q by more fine-grained -q;
2009-07-20, by wenzelm
merged
2009-07-20, by wenzelm
merged
2009-07-20, by haftmann
closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
2009-07-20, by haftmann
merged
2009-07-15, by haftmann
merged
2009-07-20, by haftmann
simplification of locale interfaces
2009-07-15, by haftmann
additional preprocessor rule
2009-07-15, by haftmann
added code_unfold_post attribute
2009-07-14, by haftmann
more accessors to unfold simpset
2009-07-14, by haftmann
clarified code
2009-07-14, by haftmann
prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14, by haftmann
tuned code annotations
2009-07-14, by haftmann
more canonical import
2009-07-14, by haftmann
merged
2009-07-14, by haftmann
merged
2009-07-14, by haftmann
refinement of lattice classes
2009-07-14, by haftmann
removed outdated comment
2009-07-13, by haftmann
Proof.future_proof: declare all assumptions as well;
2009-07-20, by wenzelm
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19, by wenzelm
cancel_proofs: some attempts at reworking group management (based on body promises only);
2009-07-19, by wenzelm
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
2009-07-19, by wenzelm
more abstract Future.is_worker;
2009-07-19, by wenzelm
tuned;
2009-07-19, by wenzelm
future_result: explicitly impose Variable.sorts_of again;
2009-07-19, by wenzelm
recovered a version of dequeue_towards (cf. bb7b5a5942c7);
2009-07-19, by wenzelm
added join_bodies;
2009-07-18, by wenzelm
scheduler: tuned tracing (status);
2009-07-18, by wenzelm
added group_id;
2009-07-18, by wenzelm
synchronized: tuned tracing;
2009-07-18, by wenzelm
tuned;
2009-07-18, by wenzelm
tuned prf_subst: use structure Same;
2009-07-18, by wenzelm
merged
2009-07-17, by wenzelm
Changed fact_Suc_nat back to fact_Suc
2009-07-17, by avigad
merged
2009-07-17, by wenzelm
merged
2009-07-17, by berghofe
merged
2009-07-15, by berghofe
commit merge
2009-07-14, by avigad
Repairs regarding new Fact.thy.
2009-07-14, by avigad
merged
2009-07-14, by berghofe
merged
2009-07-14, by berghofe
Use term antiquotation to refer to constant names in subsection title.
2009-07-14, by berghofe
Repaired uses of factorial.
2009-07-10, by avigad
Automated merge with http://isabelle.in.tum.de/repos/isabelle
2009-07-10, by avigad
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
2009-07-10, by avigad
tuned/modernized Envir.subst_XXX;
2009-07-17, by wenzelm
tuned/modernized subst: Same.operation;
2009-07-17, by wenzelm
tuned;
2009-07-17, by wenzelm
tuned/modernized Envir operations;
2009-07-17, by wenzelm
major cleanup, simplification, modernization;
2009-07-17, by wenzelm
eq_type: special case for empty environment;
2009-07-17, by wenzelm
compare types directly -- no need to invoke Type.eq_type with empty environment;
2009-07-17, by wenzelm
incr_indexes (from Proofterm);
2009-07-16, by wenzelm
tuned incr_indexes;
2009-07-16, by wenzelm
tuned incr_tvar_same;
2009-07-16, by wenzelm
added same;
2009-07-16, by wenzelm
tuned map_proof_terms_option;
2009-07-16, by wenzelm
export incr_tvar_same;
2009-07-16, by wenzelm
added map_option;
2009-07-16, by wenzelm
use structure Same;
2009-07-16, by wenzelm
use structure Same;
2009-07-16, by wenzelm
use structure Same;
2009-07-16, by wenzelm
use structure Same;
2009-07-16, by wenzelm
added map;
2009-07-16, by wenzelm
use structure Same;
2009-07-16, by wenzelm
Support for copy-avoiding functions on pure values, at the cost of readability.
2009-07-16, by wenzelm
removed obsolete/unused legacy_varify;
2009-07-16, by wenzelm
eliminated legacy_varify;
2009-07-16, by wenzelm
merged
2009-07-15, by wenzelm
simplified proofs
2009-07-15, by Christian Urban
more antiquotations;
2009-07-15, by wenzelm
eliminated obsolete legacy_varify;
2009-07-15, by wenzelm
tuned comment;
2009-07-15, by wenzelm
Made "prime" executable
2009-07-15, by nipkow
More finite set induction rules
2009-07-15, by nipkow
made upt/upto executable on nat/int by simp
2009-07-15, by nipkow
removed obsolete/unused legacy_unvarify;
2009-07-14, by wenzelm
tuned prepare_patternT: Term.exists_subtype;
2009-07-14, by wenzelm
tuned paramify_vars: Term_Subst.map_atypsT_option;
2009-07-14, by wenzelm
merged
2009-07-14, by haftmann
updated to changes in sources; tuned
2009-07-14, by haftmann
updated to changes in sources; tuned
2009-07-14, by haftmann
code attributes use common underscore convention
2009-07-14, by haftmann
NEWS and CONTRIBUTORS
2009-07-14, by haftmann
Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
2009-07-13, by berghofe
more gcd/lcm lemmas
2009-07-12, by nipkow
typo
2009-07-12, by nipkow
resolvd conflict
2009-07-12, by nipkow
More about gcd/lcm, and some cleaning up
2009-07-12, by nipkow
added boolean_algebra type class; tuned lattice duals
2009-07-11, by haftmann
move Kleene_Algebra to Library
2009-07-10, by krauss
merged
2009-07-10, by haftmann
tuned locale interface
2009-07-10, by haftmann
tuned
2009-07-10, by haftmann
dropped find_index_eq
2009-07-10, by haftmann
tuned quickcheck generator for bool
2009-07-10, by haftmann
tuned
2009-07-10, by haftmann
merged
2009-07-10, by wenzelm
merged
2009-07-10, by wenzelm
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
2009-07-10, by wenzelm
added some generic mapping combinators;
2009-07-10, by wenzelm
reorganised; many new lemmas thanks to sledgehammer
2009-07-09, by krauss
tuned
2009-07-09, by krauss
renamed structure TermSubst to Term_Subst;
2009-07-09, by wenzelm
Sorttab in Pure;
2009-07-09, by wenzelm
removed obsolete CVS Ids;
2009-07-09, by wenzelm
removed obsolete CVS Ids;
2009-07-09, by wenzelm
merged
2009-07-09, by wenzelm
recovered some proofs broken in 0314441a53a6;
2009-07-09, by wenzelm
renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-09, by wenzelm
move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
2009-07-09, by krauss
drop unused lemmas
2009-07-09, by krauss
FPS form a metric space, which justifies the infinte sum notation
2009-07-09, by chaieb
merged
2009-07-09, by chaieb
merged
2009-07-05, by chaieb
merged
2009-07-04, by chaieb
merged
2009-07-04, by chaieb
Gettring rid of sorts hyps
2009-07-02, by chaieb
tuned structure Code internally
2009-07-08, by haftmann
merged
2009-07-08, by nipkow
name fixed
2009-07-08, by nipkow
merged
2009-07-07, by haftmann
merged
2009-07-07, by haftmann
tuned interface of structure Code
2009-07-07, by haftmann
more accurate certificates for constant aliasses
2009-07-07, by haftmann
merged
2009-07-07, by haftmann
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
2009-07-07, by haftmann
fixed proof (cf. 40501bb2d57c);
2009-07-07, by wenzelm
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-07-07, by nipkow
merged
2009-07-07, by haftmann
tuned code
2009-07-06, by haftmann
moved Inductive.myinv to Fun.inv; tuned
2009-07-06, by haftmann
add_classrel/arity: strip_shyps of stored result;
2009-07-07, by wenzelm
clarified strip_shyps: proper type witnesses for present sorts;
2009-07-06, by wenzelm
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-07-06, by wenzelm
structure Thm: less pervasive names;
2009-07-06, by wenzelm
clarified Thm.of_class/of_sort/class_triv;
2009-07-06, by wenzelm
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-06, by wenzelm
renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
2009-07-04, by wenzelm
Delayed action.
2009-07-04, by wenzelm
merged
2009-07-04, by wenzelm
merged
2009-07-04, by haftmann
nominal.ML is nominal_datatype.ML
2009-07-03, by haftmann
merged
2009-07-03, by haftmann
nominal.ML is nominal_datatype.ML
2009-07-03, by haftmann
cleaned up fundamental iml term functions; nested patterns
2009-07-03, by haftmann
cleaned up fundamental iml term functions
2009-07-03, by haftmann
proper closures -- imperative programming considered harmful...
2009-07-03, by haftmann
avoid useless code equations
2009-07-03, by haftmann
restored subscripts
2009-07-03, by haftmann
lemma foldl_apply_inv
2009-07-03, by haftmann
is_open: surrogate sequence is High..Low;
2009-07-04, by wenzelm
init/check Isabelle_System;
2009-07-03, by wenzelm
init isabelle home from existing setting or hint via system property;
2009-07-03, by wenzelm
more hgignore;
2009-07-03, by wenzelm
basic setup for Isabelle/JVM application bundle;
2009-07-03, by wenzelm
separate setup for App1;
2009-07-03, by wenzelm
SCALA_HOME: proper line escapes for choosefrom;
2009-07-03, by wenzelm
allow reloading of settings within JVM process;
2009-07-03, by wenzelm
Isabelle application wrapper for windows.
2009-07-03, by wenzelm
isabelle.home: native jvmpath;
2009-07-03, by wenzelm
Generic Isabelle application wrapper.
2009-07-03, by wenzelm
observe SCALA_HOME, if available;
2009-07-03, by wenzelm
merged
2009-07-02, by wenzelm
recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
2009-07-02, by wenzelm
merged
2009-07-02, by haftmann
instance arities can be simultaneous
2009-07-02, by haftmann
updated generated files
2009-07-02, by haftmann
more friendly wrt. PGs interpretation of compound *); added dedicated section on value and quickcheck
2009-07-02, by haftmann
merged
2009-07-02, by paulson
Deleted some debugging code
2009-07-02, by paulson
merged
2009-07-01, by paulson
merged
2009-06-24, by paulson
merged
2009-06-23, by paulson
Removed unnecessary conditions concerning nonzero divisors
2009-06-18, by paulson
strip_shyps: remove top sort, which is logically insignificant;
2009-07-02, by wenzelm
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-07-02, by wenzelm
added pro-forma proof constructor Inclass;
2009-07-02, by wenzelm
renamed NamedThmsFun to Named_Thms;
2009-07-02, by wenzelm
renamed NamedThmsFun to Named_Thms;
2009-07-02, by wenzelm
misc tuning;
2009-07-02, by wenzelm
fixed document (DERIV_intros);
2009-07-02, by wenzelm
more detailed timing message;
2009-06-30, by wenzelm
default to maximum max_threads;
2009-06-30, by wenzelm
merged
2009-06-30, by wenzelm
fixed ISABELLE_HOME_USER;
2009-06-30, by wenzelm
merged
2009-06-30, by haftmann
adaptated to changes in term representation
2009-06-30, by haftmann
improved treatment of case patterns
2009-06-30, by haftmann
merged
2009-06-30, by haftmann
an intermediate step towards a refined translation of cases
2009-06-30, by haftmann
all variable names are optional
2009-06-30, by haftmann
variable names in abstractions are optional
2009-06-30, by haftmann
restored
2009-06-30, by haftmann
added isatest for x86_64-darwin;
2009-06-30, by wenzelm
merged
2009-06-30, by wenzelm
NEWS updated
2009-06-30, by hoelzl
DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln.
2009-06-30, by hoelzl
remove DERIV_tac and deriv_tac, neither is used in Isabelle/HOL or the AFP
2009-06-30, by hoelzl
use DERIV_intros
2009-06-30, by hoelzl
Added DERIV_intros
2009-06-30, by hoelzl
commented trancl example; added debug message
2009-06-30, by bulwahn
merged
2009-06-30, by bulwahn
exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler
2009-06-30, by bulwahn
added diagnostic printing; changed proof for parameters; moved code
2009-06-29, by bulwahn
merged
2009-06-30, by haftmann
simplified binding concept
2009-06-30, by haftmann
temporary workaround
2009-06-30, by haftmann
tuned
2009-06-30, by haftmann
streamlined code
2009-06-30, by haftmann
dropped id
2009-06-30, by haftmann
mutual instances
2009-06-29, by haftmann
canonical prefix for datatype derivates
2009-06-29, by haftmann
tuned
2009-06-29, by haftmann
check for correct proof output
2009-06-30, by immler
fixed: count constants with supplementary lemmas
2009-06-30, by immler
removed latex markup - there is no document generated from Decision_Procs/ex
2009-06-30, by hoelzl
Implemented taylor series expansion for approximation
2009-06-29, by hoelzl
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
2009-06-30, by wenzelm
merged
2009-06-30, by wenzelm
more display;
2009-06-30, by wenzelm
added icon;
2009-06-30, by wenzelm
basic launch4j setup;
2009-06-30, by wenzelm
fixed permissions;
2009-06-30, by wenzelm
fixed permissions;
2009-06-30, by wenzelm
Corrected handling of bound variables.
2009-06-29, by berghofe
merged
2009-06-29, by haftmann
dropped Id
2009-06-29, by haftmann
explicit Set constructor for code generated for sets
2009-06-29, by haftmann
hide popular names
2009-06-29, by haftmann
Executable_Set is now a simple wrapper around Fset
2009-06-29, by haftmann
renamed theory Code_Set to Fset
2009-06-29, by haftmann
updated generated document
2009-06-29, by haftmann
Executable_Set now based on Code_Set
2009-06-28, by haftmann
added Inter, Union
2009-06-28, by haftmann
more precise dependencies for "jars";
2009-06-28, by wenzelm
improved display;
2009-06-28, by wenzelm