Sun, 25 Apr 2010 00:25:44 +0200 blanchet remove "show_skolems" option and change style of record declarations
Sun, 25 Apr 2010 00:10:30 +0200 blanchet remove "skolemize" option from Nitpick, since Skolemization is always useful
Sat, 24 Apr 2010 17:48:21 +0200 blanchet removed Nitpick's "uncurry" option
Sat, 24 Apr 2010 16:44:45 +0200 blanchet fix typesetting
Sat, 24 Apr 2010 16:43:03 +0200 blanchet Fruhjahrsputz: remove three mostly useless Nitpick options
Sat, 24 Apr 2010 16:33:01 +0200 blanchet remove type annotations as comments;
Sat, 24 Apr 2010 16:17:30 +0200 blanchet cosmetics
Sat, 24 Apr 2010 16:05:42 +0200 blanchet better error reporting;
Fri, 23 Apr 2010 19:36:49 +0200 blanchet cosmetics
Fri, 23 Apr 2010 19:26:39 +0200 blanchet reuse timestamp function
Fri, 23 Apr 2010 19:18:39 +0200 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
Fri, 23 Apr 2010 19:16:52 +0200 blanchet make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
Fri, 23 Apr 2010 19:12:49 +0200 blanchet remove some bloat
Fri, 23 Apr 2010 18:11:41 +0200 blanchet now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
Fri, 23 Apr 2010 18:06:41 +0200 blanchet renamed module "ATP_Wrapper" to "ATP_Systems"
Fri, 23 Apr 2010 17:38:25 +0200 blanchet move the minimizer to the Sledgehammer directory
Fri, 23 Apr 2010 16:59:48 +0200 blanchet remove debugging code
Fri, 23 Apr 2010 16:55:51 +0200 blanchet move some sledgehammer stuff out of "atp_manager.ML"
Fri, 23 Apr 2010 16:21:47 +0200 blanchet give an error if no ATP is set
Fri, 23 Apr 2010 16:15:35 +0200 blanchet move the Sledgehammer menu options to "sledgehammer_isar.ML"
Fri, 23 Apr 2010 15:48:34 +0200 blanchet centralized ATP-specific error handling in "atp_wrapper.ML"
Fri, 23 Apr 2010 13:16:50 +0200 blanchet handle ATP proof delimiters in a cleaner, more extensible fashion
Mon, 26 Apr 2010 22:59:28 +0200 wenzelm merged
Mon, 26 Apr 2010 11:08:49 -0700 huffman fix another if-then-else parse error
Mon, 26 Apr 2010 10:57:04 -0700 huffman fix if-then-else parse error
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:37:46 -0700 huffman fix syntax precedence declarations for UNION, INTER, SUP, INF
Mon, 26 Apr 2010 09:26:31 -0700 huffman syntax precedence for If and Let
Mon, 26 Apr 2010 09:21:25 -0700 huffman fix lots of looping simp calls and other warnings
Sun, 25 Apr 2010 23:22:29 -0700 huffman fix duplicate simp rule warnings
Sun, 25 Apr 2010 20:48:19 -0700 huffman define finer-than ordering on net type; move some theorems into Limits.thy
Sun, 25 Apr 2010 16:23:40 -0700 huffman generalize type of continuous_on
Sun, 25 Apr 2010 11:58:39 -0700 huffman define nets directly as filters, instead of as filter bases
Mon, 26 Apr 2010 21:50:28 +0200 wenzelm use 'example_proof' (invisible);
Mon, 26 Apr 2010 21:45:08 +0200 wenzelm command 'example_proof' opens an empty proof body;
Mon, 26 Apr 2010 21:36:44 +0200 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;
Mon, 26 Apr 2010 20:30:50 +0200 wenzelm eliminanated some unreferenced identifiers;
Mon, 26 Apr 2010 16:08:04 +0200 wenzelm merged
Mon, 26 Apr 2010 15:14:14 +0200 Cezary Kaliszyk add bounded_lattice_bot and bounded_lattice_top type classes
Mon, 26 Apr 2010 13:43:31 +0200 haftmann merged
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Mon, 26 Apr 2010 11:34:15 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
Mon, 26 Apr 2010 11:34:15 +0200 haftmann line break
Mon, 26 Apr 2010 14:44:41 +0200 wenzelm removed unused AxClass.class_intros;
Mon, 26 Apr 2010 11:20:18 +0200 wenzelm updated Sign.add_type_abbrev;
Mon, 26 Apr 2010 07:47:18 +0200 haftmann merged
Sun, 25 Apr 2010 08:25:34 +0200 haftmann field_simps as named theorems
Sun, 25 Apr 2010 23:26:40 +0200 wenzelm merged
Sun, 25 Apr 2010 10:23:03 -0700 huffman generalize more constants and lemmas
Sun, 25 Apr 2010 09:01:03 -0700 huffman simplify types of path operations (use real instead of real^1)
Sun, 25 Apr 2010 07:41:57 -0700 huffman add lemmas convex_real_interval and convex_box
Sat, 24 Apr 2010 21:29:22 -0700 huffman generalize more constants and lemmas
Sat, 24 Apr 2010 19:32:20 -0700 huffman generalize constant closest_point
Sat, 24 Apr 2010 14:06:19 -0700 huffman minimize imports
Sat, 24 Apr 2010 13:34:11 -0700 huffman fix imports
Sat, 24 Apr 2010 13:31:52 -0700 huffman document generation for Multivariate_Analysis
Sat, 24 Apr 2010 11:11:09 -0700 huffman move l2-norm stuff into separate theory file
Sat, 24 Apr 2010 09:37:24 -0700 huffman convert proofs to Isar-style
Sat, 24 Apr 2010 09:34:36 -0700 huffman Library/Fraction_Field.thy: ordering relations for fractions
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip