Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
display some platform information;
2009-06-28, by wenzelm
discontinued separate "pdf" archive -- since it is now relatively small compared to the main archive, there is no point to fragment things;
2009-06-28, by wenzelm
merged
2009-06-28, by wenzelm
check if conjectures have been used in proof
2009-06-28, by immler
return number of first conjecture-clause and number of conjecture-clauses;
2009-06-28, by immler
use structure File instead of TextIO;
2009-06-28, by immler
whitelist for HOL problems with ext:
2009-06-28, by immler
always include whitelist;
2009-06-28, by immler
check for current versions on server
2009-06-28, by immler
relevance filter with the same parameters for remote-versions
2009-06-28, by immler
use X2TPTP optionally and only for remote_spass;
2009-06-28, by immler
fixed
2009-06-28, by immler
clarified "jars" target;
2009-06-28, by wenzelm
produce self-contained isabelle-scala.jar;
2009-06-28, by wenzelm
proper interpretation of Cygwin.config;
2009-06-28, by wenzelm
sane platform look-and-feel;
2009-06-28, by wenzelm
minimal GUI_Setup, which is the main class of Pure.jar;
2009-06-28, by wenzelm
some more Cygwin checks;
2009-06-28, by wenzelm
moved platform identification to platform.scala;
2009-06-28, by wenzelm
less ambitious version that works with Java 1.5;
2009-06-27, by wenzelm
clarified default_platform;
2009-06-27, by wenzelm
more detailed platform identification;
2009-06-27, by wenzelm
isabelle_path: slightly more liberal root pattern;
2009-06-27, by wenzelm
added isabelle_path;
2009-06-27, by wenzelm
tune File.isabelle_tool signature;
2009-06-27, by wenzelm
builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
2009-06-27, by wenzelm
removed old primrecs
2009-06-27, by nipkow
replaced recdefs by funs
2009-06-27, by nipkow
tuned abbrevs;
2009-06-26, by wenzelm
lcm abs lemmas
2009-06-26, by nipkow
gcd abs lemmas
2009-06-26, by nipkow
NEWS updated
2009-06-25, by hoelzl
Improved computation of bounds and implemented interval splitting for 'approximation'.
2009-06-25, by hoelzl
Added new evaluator "approximate"
2009-06-08, by hoelzl
tuned
2009-06-15, by hoelzl
merged
2009-06-25, by haftmann
added List_Set and Code_Set theories
2009-06-25, by haftmann
merged
2009-06-25, by wenzelm
merged
2009-06-25, by haftmann
arbitrary farewell
2009-06-25, by haftmann
expand_path: handle parent (..) elements;
2009-06-25, by wenzelm
more stats;
2009-06-25, by wenzelm
merged
2009-06-25, by wenzelm
Streamlined code
2009-06-25, by nipkow
merged
2009-06-25, by nipkow
Cleaned up GCD
2009-06-25, by nipkow
renamed IsabelleProcess to Isabelle_Process;
2009-06-25, by wenzelm
renamed IsabelleSystem to Isabelle_System;
2009-06-25, by wenzelm
standard naming conventions for session and theories;
2009-06-24, by wenzelm
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-24, by wenzelm
proper ML interface set_full_types;
2009-06-24, by wenzelm
Replaced Suc_remove by Suc_eq_plus1
2009-06-24, by nipkow
New ATP option: full types
2009-06-24, by nipkow
corrected and unified thm names
2009-06-24, by nipkow
merged
2009-06-23, by haftmann
merged
2009-06-23, by haftmann
Datatype.get_all
2009-06-23, by haftmann
corrected handling of free variables in arguments
2009-06-23, by haftmann
tuned proof
2009-06-23, by haftmann
tuned interfaces of datatype module
2009-06-23, by haftmann
add_datatypes does not yield particular rules any longer
2009-06-23, by haftmann
merged
2009-06-23, by haftmann
add_datatype interface yields type names and less rules
2009-06-23, by haftmann
non-public representation;
2009-06-23, by wenzelm
fixed abbrev !! for \<And>;
2009-06-23, by wenzelm
merged
2009-06-23, by wenzelm
merged
2009-06-23, by haftmann
simplified proof
2009-06-23, by haftmann
uniformly capitialized names for subdirectories
2009-06-23, by haftmann
renamed ioa to automaton
2009-06-23, by haftmann
renamed ioa to automaton
2009-06-23, by haftmann
dropped duplicated lemmas, tuned header
2009-06-23, by haftmann
NewNumberTheory depends on Algebra
2009-06-23, by haftmann
merged
2009-06-23, by haftmann
lemma funcset_id by Jeremy Avigad
2009-06-23, by haftmann
lemma finite_image_set by Jeremy Avigad
2009-06-23, by haftmann
merged
2009-06-23, by nipkow
new lemmas
2009-06-23, by nipkow
tuned input: require longer symbol prefix;
2009-06-23, by wenzelm
moved string utilities to completion.scala;
2009-06-23, by wenzelm
Completion of symbols and keywords.
2009-06-23, by wenzelm
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
2009-06-23, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip