isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

remove type annotations as comments;
2010-04-24, by blanchet
cosmetics
2010-04-24, by blanchet
better error reporting;
2010-04-24, by blanchet
cosmetics
2010-04-23, by blanchet
reuse timestamp function
2010-04-23, by blanchet
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-04-23, by blanchet
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
2010-04-23, by blanchet
remove some bloat
2010-04-23, by blanchet
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
2010-04-23, by blanchet
renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23, by blanchet
move the minimizer to the Sledgehammer directory
2010-04-23, by blanchet
remove debugging code
2010-04-23, by blanchet
move some sledgehammer stuff out of "atp_manager.ML"
2010-04-23, by blanchet
give an error if no ATP is set
2010-04-23, by blanchet
move the Sledgehammer menu options to "sledgehammer_isar.ML"
2010-04-23, by blanchet
centralized ATP-specific error handling in "atp_wrapper.ML"
2010-04-23, by blanchet
handle ATP proof delimiters in a cleaner, more extensible fashion
2010-04-23, by blanchet
merged
2010-04-26, by wenzelm
fix another if-then-else parse error
2010-04-26, by huffman
fix if-then-else parse error
2010-04-26, by huffman
merged
2010-04-26, by huffman
fix syntax precedence declarations for UNION, INTER, SUP, INF
2010-04-26, by huffman
syntax precedence for If and Let
2010-04-26, by huffman
fix lots of looping simp calls and other warnings
2010-04-26, by huffman
fix duplicate simp rule warnings
2010-04-25, by huffman
define finer-than ordering on net type; move some theorems into Limits.thy
2010-04-25, by huffman
generalize type of continuous_on
2010-04-25, by huffman
define nets directly as filters, instead of as filter bases
2010-04-25, by huffman
use 'example_proof' (invisible);
2010-04-26, by wenzelm
command 'example_proof' opens an empty proof body;
2010-04-26, by wenzelm
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
2010-04-26, by wenzelm
eliminanated some unreferenced identifiers;
2010-04-26, by wenzelm
merged
2010-04-26, by wenzelm
add bounded_lattice_bot and bounded_lattice_top type classes
2010-04-26, by Cezary Kaliszyk
merged
2010-04-26, by haftmann
dropped group_simps, ring_simps, field_eq_simps
2010-04-26, by haftmann
class division_ring_inverse_zero
2010-04-26, by haftmann
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-26, by haftmann
line break
2010-04-26, by haftmann
removed unused AxClass.class_intros;
2010-04-26, by wenzelm
updated Sign.add_type_abbrev;
2010-04-26, by wenzelm
merged
2010-04-26, by haftmann
field_simps as named theorems
2010-04-25, by haftmann
merged
2010-04-25, by wenzelm
generalize more constants and lemmas
2010-04-25, by huffman
simplify types of path operations (use real instead of real^1)
2010-04-25, by huffman
add lemmas convex_real_interval and convex_box
2010-04-25, by huffman
generalize more constants and lemmas
2010-04-24, by huffman
generalize constant closest_point
2010-04-24, by huffman
minimize imports
2010-04-24, by huffman
fix imports
2010-04-24, by huffman
document generation for Multivariate_Analysis
2010-04-24, by huffman
move l2-norm stuff into separate theory file
2010-04-24, by huffman
convert proofs to Isar-style
2010-04-24, by huffman
Library/Fraction_Field.thy: ordering relations for fractions
2010-04-24, by huffman
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-04-25, by wenzelm
more systematic treatment of data -- avoid slightly odd nested tuples here;
2010-04-25, by wenzelm
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25, by wenzelm
misc tuning and simplification;
2010-04-25, by wenzelm
simplified some private bindings;
2010-04-25, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle