isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -112 +112 +1000 +3000 +10000 +30000 tip

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