| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
moved generic List operations to theory More_List
|
changeset |
files
|
| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
adjusted
|
changeset |
files
|
| Thu, 20 May 2010 16:35:52 +0200 |
haftmann |
turned old-style mem into an input abbreviation
|
changeset |
files
|
| Thu, 20 May 2010 23:20:01 +0200 |
wenzelm |
zoom font size;
|
changeset |
files
|
| Thu, 20 May 2010 23:19:28 +0200 |
wenzelm |
added somewhat generic zoom box;
|
changeset |
files
|
| Thu, 20 May 2010 21:32:48 +0200 |
wenzelm |
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
|
changeset |
files
|
| Thu, 20 May 2010 21:10:03 +0200 |
wenzelm |
mutate displayed document synchronously in Swing thread, for improved robustness;
|
changeset |
files
|
| Thu, 20 May 2010 21:07:05 +0200 |
wenzelm |
read style sheets only once;
|
changeset |
files
|
| Thu, 20 May 2010 20:56:26 +0200 |
wenzelm |
handle component resize for output / HTML panel;
|
changeset |
files
|
| Thu, 20 May 2010 20:22:00 +0200 |
wenzelm |
Isabelle_System: allow explicit isabelle_home argument;
|
changeset |
files
|
| Thu, 20 May 2010 20:20:52 +0200 |
wenzelm |
enable shell script editor mode;
|
changeset |
files
|
| Thu, 20 May 2010 16:25:22 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 20 May 2010 07:36:50 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Thu, 20 May 2010 07:34:45 +0200 |
bulwahn |
deactivated timing of infering modes
|
changeset |
files
|
| Wed, 19 May 2010 18:24:09 +0200 |
bulwahn |
adapting examples
|
changeset |
files
|
| Wed, 19 May 2010 18:24:09 +0200 |
bulwahn |
changing operations for accessing data to work with contexts
|
changeset |
files
|
| Wed, 19 May 2010 18:24:08 +0200 |
bulwahn |
removed unnecessary Thm.transfer in the predicate compiler
|
changeset |
files
|
| Wed, 19 May 2010 18:24:07 +0200 |
bulwahn |
changing compilation to work only with contexts; adapting quickcheck
|
changeset |
files
|
| Wed, 19 May 2010 18:24:06 +0200 |
bulwahn |
removing unused argument in print_modes function
|
changeset |
files
|
| Wed, 19 May 2010 18:24:05 +0200 |
bulwahn |
moving towards working with proof contexts in the predicate compiler
|
changeset |
files
|
| Wed, 19 May 2010 18:24:04 +0200 |
bulwahn |
improved values command to handle a special case with tuples and polymorphic predicates more correctly
|
changeset |
files
|
| Wed, 19 May 2010 18:24:03 +0200 |
bulwahn |
improved behaviour of defined_functions in the predicate compiler
|
changeset |
files
|
| Wed, 19 May 2010 17:01:07 -0700 |
huffman |
move some example files into new HOLCF/Tutorial directory
|
changeset |
files
|
| Wed, 19 May 2010 16:28:24 -0700 |
huffman |
remove redundant hdvd relation
|
changeset |
files
|
| Wed, 19 May 2010 16:08:41 -0700 |
huffman |
remove unnecessary constant Fixrec.bind
|
changeset |
files
|
| Wed, 19 May 2010 14:38:25 -0700 |
huffman |
add section about fixrec definitions with looping simp rules
|
changeset |
files
|
| Wed, 19 May 2010 13:07:15 -0700 |
huffman |
more informative error message for fixrec when continuity proof fails
|
changeset |
files
|
| Thu, 20 May 2010 16:22:50 +0200 |
wenzelm |
determine margin just before rendering -- proper reformatting when updating;
|
changeset |
files
|
| Thu, 20 May 2010 15:51:28 +0200 |
wenzelm |
simplified alignment via FlowPanel;
|
changeset |
files
|
| Thu, 20 May 2010 13:54:31 +0200 |
wenzelm |
more systematic treatment of physical document wrt. font size etc.;
|
changeset |
files
|
| Thu, 20 May 2010 11:44:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 20 May 2010 11:36:30 +0200 |
wenzelm |
general Isabelle_System.try_read;
|
changeset |
files
|
| Thu, 20 May 2010 10:43:46 +0200 |
wenzelm |
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
|
changeset |
files
|
| Thu, 20 May 2010 10:31:20 +0200 |
wenzelm |
inverted "Freeze" to "Follow", which is the default;
|
changeset |
files
|
| Wed, 19 May 2010 21:18:02 +0200 |
wenzelm |
basic controls to freeze/update prover results;
|
changeset |
files
|
| Wed, 19 May 2010 18:05:34 +0200 |
wenzelm |
show fully detailed protocol messages;
|
changeset |
files
|
| Wed, 19 May 2010 17:39:22 +0200 |
wenzelm |
some updates following src/Tools/jEdit/dist-template/settings;
|
changeset |
files
|
| Wed, 19 May 2010 12:35:20 +0200 |
haftmann |
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
|
changeset |
files
|
| Wed, 19 May 2010 10:17:31 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 19 May 2010 10:17:05 +0200 |
haftmann |
dropped legacy_unconstrainT
|
changeset |
files
|
| Wed, 19 May 2010 10:14:37 +0200 |
haftmann |
new version of triv_of_class machinery without legacy_unconstrain
|
changeset |
files
|
| Wed, 19 May 2010 09:21:30 +0200 |
haftmann |
merge
|
changeset |
files
|
| Wed, 19 May 2010 09:20:36 +0200 |
haftmann |
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
|
changeset |
files
|
| Tue, 18 May 2010 19:00:55 -0700 |
huffman |
remove several redundant lemmas about floor and ceiling
|
changeset |
files
|
| Tue, 18 May 2010 06:28:42 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
changeset |
files
|
| Mon, 17 May 2010 18:51:25 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Mon, 17 May 2010 16:52:34 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Mon, 17 May 2010 15:58:32 -0700 |
huffman |
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
|
changeset |
files
|
| Tue, 18 May 2010 10:13:33 +0200 |
wenzelm |
prefer structure Keyword and Parse;
|
changeset |
files
|
| Tue, 18 May 2010 00:01:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 17 May 2010 12:00:10 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 17 May 2010 08:45:46 -0700 |
huffman |
remove simp attribute from square_eq_1_iff
|
changeset |
files
|
| Mon, 17 May 2010 17:50:09 +0200 |
blanchet |
merged
|
changeset |
files
|
| Mon, 17 May 2010 15:21:11 +0200 |
blanchet |
make sure chained facts don't pop up in the metis proof
|
changeset |
files
|
| Mon, 17 May 2010 12:15:37 +0200 |
blanchet |
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
|
changeset |
files
|
| Mon, 17 May 2010 10:18:14 +0200 |
blanchet |
generate proper arity declarations for TFrees for SPASS's DFG format;
|
changeset |
files
|
| Mon, 17 May 2010 10:16:54 +0200 |
blanchet |
identify common SPASS error more clearly
|
changeset |
files
|
| Mon, 17 May 2010 08:40:17 -0700 |
huffman |
remove simp attribute from power2_eq_1_iff
|
changeset |
files
|
| Mon, 17 May 2010 10:58:58 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
changeset |
files
|
| Mon, 17 May 2010 10:58:31 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
changeset |
files
|
| Tue, 18 May 2010 00:01:03 +0200 |
wenzelm |
do not open Legacy by default;
|
changeset |
files
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
changeset |
files
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
changeset |
files
|
| Mon, 17 May 2010 15:05:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 May 2010 15:02:44 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 17 May 2010 14:23:54 +0200 |
wenzelm |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
changeset |
files
|
| Mon, 17 May 2010 10:20:55 +0200 |
wenzelm |
centralized legacy aliases;
|
changeset |
files
|
| Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
changeset |
files
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
changeset |
files
|
| Sat, 15 May 2010 23:32:15 +0200 |
wenzelm |
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
|
changeset |
files
|
| Sat, 15 May 2010 23:23:45 +0200 |
wenzelm |
renamed structure ValueParse to Parse_Value;
|
changeset |
files
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
changeset |
files
|
| Sat, 15 May 2010 22:24:25 +0200 |
wenzelm |
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
|
changeset |
files
|
| Sat, 15 May 2010 22:15:57 +0200 |
wenzelm |
renamed Outer_Parse to Parse (in Scala);
|
changeset |
files
|
| Sat, 15 May 2010 22:05:49 +0200 |
wenzelm |
renamed Outer_Keyword to Keyword (in Scala);
|
changeset |
files
|
| Sat, 15 May 2010 21:57:27 +0200 |
wenzelm |
avoid open Conv;
|
changeset |
files
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
changeset |
files
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
changeset |
files
|
| Sat, 15 May 2010 21:09:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 May 2010 18:29:18 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 15 May 2010 07:48:24 -0700 |
huffman |
add real_le_linear to list of legacy theorem names
|
changeset |
files
|
| Sat, 15 May 2010 16:20:54 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Sat, 15 May 2010 18:15:50 +0200 |
wenzelm |
removed unused conversions;
|
changeset |
files
|
| Sat, 15 May 2010 18:12:58 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Sat, 15 May 2010 18:11:00 +0200 |
wenzelm |
moved normarith.ML where it is actually used;
|
changeset |
files
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
changeset |
files
|
| Sat, 15 May 2010 15:31:33 +0200 |
wenzelm |
eliminated redundant runtime checks;
|
changeset |
files
|
| Sat, 15 May 2010 00:45:42 +0200 |
krauss |
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
|
changeset |
files
|
| Sat, 15 May 2010 15:07:39 +0200 |
wenzelm |
more precise dependencies for HOL-Word-SMT_Examples;
|
changeset |
files
|
| Sat, 15 May 2010 13:31:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 14 May 2010 23:35:35 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 14 May 2010 23:34:24 +0200 |
blanchet |
added Sledgehammer documentation to TOC
|
changeset |
files
|
| Fri, 14 May 2010 23:32:48 +0200 |
blanchet |
added some Sledgehammer news
|
changeset |
files
|
| Fri, 14 May 2010 23:16:33 +0200 |
blanchet |
document Nitpick changes
|
changeset |
files
|
| Fri, 14 May 2010 22:43:24 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 14 May 2010 22:43:00 +0200 |
blanchet |
added Sledgehammer manual;
|
changeset |
files
|
| Fri, 14 May 2010 22:30:24 +0200 |
blanchet |
renamed Sledgehammer options
|
changeset |
files
|
| Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
changeset |
files
|
| Fri, 14 May 2010 22:28:39 +0200 |
blanchet |
remove support for crashing beta solver HaifaSat
|
changeset |
files
|
| Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
changeset |
files
|
| Fri, 14 May 2010 22:46:58 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 14 May 2010 22:46:41 +0200 |
nipkow |
added listsum lemmas
|
changeset |
files
|
| Fri, 14 May 2010 21:23:29 +0200 |
ballarin |
Revert mixin patch due to inacceptable performance drop.
|
changeset |
files
|
| Fri, 14 May 2010 15:27:07 +0200 |
blanchet |
add "no_atp"s to Nitpick lemmas
|
changeset |
files
|
| Fri, 14 May 2010 15:26:26 +0200 |
blanchet |
query _HOME environment variables at run-time, not at build-time
|
changeset |
files
|
| Fri, 14 May 2010 15:09:37 +0200 |
blanchet |
move Refute dependency from Plain to Main
|
changeset |
files
|
| Fri, 14 May 2010 15:07:53 +0200 |
blanchet |
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
|
changeset |
files
|
| Fri, 14 May 2010 15:02:38 +0200 |
blanchet |
recognize new Kodkod error message syntax
|
changeset |
files
|
| Fri, 14 May 2010 14:14:22 +0200 |
blanchet |
improve precision of set constructs in Nitpick
|
changeset |
files
|
| Fri, 14 May 2010 12:01:16 +0200 |
blanchet |
produce more potential counterexamples for subset operator (cf. quantifiers)
|
changeset |
files
|
| Fri, 14 May 2010 11:24:49 +0200 |
blanchet |
improved Sledgehammer proofs
|
changeset |
files
|
| Fri, 14 May 2010 11:24:14 +0200 |
blanchet |
pass "full_type" argument to proof reconstruction
|
changeset |
files
|
| Fri, 14 May 2010 11:23:42 +0200 |
blanchet |
made Sledgehammer's full-typed proof reconstruction work for the first time;
|
changeset |
files
|
| Fri, 14 May 2010 11:20:09 +0200 |
blanchet |
delect installed ATPs dynamically, _not_ at image built time
|
changeset |
files
|
| Thu, 13 May 2010 15:09:42 +0200 |
ballarin |
Fix syntax; apparently constant apply was introduced in an earlier changeset.
|
changeset |
files
|
| Thu, 13 May 2010 14:47:15 +0200 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 13 May 2010 13:30:16 +0200 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
changeset |
files
|
| Thu, 13 May 2010 13:29:43 +0200 |
ballarin |
Remove improper use of mixin in class package.
|
changeset |
files
|
| Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
changeset |
files
|
| Wed, 12 May 2010 22:33:10 -0700 |
huffman |
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
|
changeset |
files
|
| Thu, 13 May 2010 00:44:48 +0200 |
boehmes |
more precise dependencies
|
changeset |
files
|
| Wed, 12 May 2010 23:54:06 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
changeset |
files
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
changeset |
files
|
| Wed, 12 May 2010 23:54:01 +0200 |
boehmes |
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
|
changeset |
files
|
| Wed, 12 May 2010 23:54:00 +0200 |
boehmes |
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:59 +0200 |
boehmes |
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:58 +0200 |
boehmes |
added tracing of reconstruction data
|
changeset |
files
|
| Wed, 12 May 2010 23:53:57 +0200 |
boehmes |
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
|
changeset |
files
|
| Wed, 12 May 2010 23:53:56 +0200 |
boehmes |
deleted SMT translation files (to be replaced by a simplified version)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:55 +0200 |
boehmes |
move the addition of extra facts into a separate module
|
changeset |
files
|
| Wed, 12 May 2010 23:53:54 +0200 |
boehmes |
normalize numerals: also rewrite Numeral0 into 0
|
changeset |
files
|
| Wed, 12 May 2010 23:53:53 +0200 |
boehmes |
added missing rewrite rules for natural min and max
|
changeset |
files
|
| Wed, 12 May 2010 23:53:52 +0200 |
boehmes |
rewrite bool case expressions as if expression
|
changeset |
files
|
| Wed, 12 May 2010 23:53:51 +0200 |
boehmes |
simplified normalize_rule and moved it further down in the code
|
changeset |
files
|
| Wed, 12 May 2010 23:53:50 +0200 |
boehmes |
merged addition of rules into one function
|
changeset |
files
|
| Wed, 12 May 2010 23:53:49 +0200 |
boehmes |
added simplification for distinctness of small lists
|
changeset |
files
|
| Wed, 12 May 2010 23:53:48 +0200 |
boehmes |
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
|
changeset |
files
|
| Fri, 14 May 2010 19:53:36 +0200 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 21:36:38 +0200 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 21:17:09 +0200 |
wenzelm |
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
|
changeset |
files
|
| Thu, 13 May 2010 20:15:59 +0200 |
wenzelm |
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
|
changeset |
files
|
| Thu, 13 May 2010 18:47:07 +0200 |
wenzelm |
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
|
changeset |
files
|
| Thu, 13 May 2010 18:22:10 +0200 |
wenzelm |
unconstrainT operations on proofs, according to krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 17:25:53 +0200 |
wenzelm |
added Proofterm.get_name variants according to krauss/schropp;
|
changeset |
files
|
| Wed, 12 May 2010 22:43:05 +0200 |
wenzelm |
conditional structure SingleAssignment;
|
changeset |
files
|
| Wed, 12 May 2010 17:10:53 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:31:43 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:27:15 +0200 |
haftmann |
tuned proofs and fact and class names
|
changeset |
files
|
| Wed, 12 May 2010 13:51:22 +0200 |
haftmann |
tuned fact collection names and some proofs
|
changeset |
files
|
| Wed, 12 May 2010 12:31:52 +0200 |
haftmann |
grouped local statements
|
changeset |
files
|
| Wed, 12 May 2010 12:31:51 +0200 |
haftmann |
tuned test problems
|
changeset |
files
|
| Wed, 12 May 2010 16:45:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:25:23 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:25:02 +0200 |
nipkow |
simplified proof
|
changeset |
files
|
| Wed, 12 May 2010 16:44:49 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Wed, 12 May 2010 15:25:58 +0200 |
wenzelm |
updated/unified some legacy warnings;
|
changeset |
files
|
| Wed, 12 May 2010 15:23:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 12 May 2010 14:52:23 +0200 |
wenzelm |
do not emit legacy_feature warnings here -- users have no chance to disable them;
|
changeset |
files
|
| Wed, 12 May 2010 14:17:26 +0200 |
wenzelm |
removed obsolete CVS Ids;
|
changeset |
files
|
| Wed, 12 May 2010 14:02:50 +0200 |
wenzelm |
removed some obsolete admin stuff;
|
changeset |
files
|
| Wed, 12 May 2010 14:02:19 +0200 |
wenzelm |
check NEWS;
|
changeset |
files
|
| Wed, 12 May 2010 13:54:49 +0200 |
wenzelm |
removed obsolete CVS Ids;
|
changeset |
files
|
| Wed, 12 May 2010 13:52:34 +0200 |
wenzelm |
updated some version numbers;
|
changeset |
files
|
| Wed, 12 May 2010 13:34:24 +0200 |
wenzelm |
minor tuning;
|
changeset |
files
|
| Wed, 12 May 2010 13:21:23 +0200 |
wenzelm |
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
|
changeset |
files
|
| Wed, 12 May 2010 12:51:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 12:20:16 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 12:09:28 +0200 |
haftmann |
modernized specifications; tuned reification
|
changeset |
files
|
| Wed, 12 May 2010 11:18:42 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 11:17:59 +0200 |
haftmann |
added lemmas concerning last, butlast, insort
|
changeset |
files
|
| Wed, 12 May 2010 11:30:18 +0200 |
Cezary Kaliszyk |
Remove RANGE_WARN
|
changeset |
files
|
| Wed, 12 May 2010 11:13:33 +0200 |
hoelzl |
clarified NEWS entry
|
changeset |
files
|
| Wed, 12 May 2010 11:08:15 +0200 |
hoelzl |
merged
|
changeset |
files
|
| Wed, 12 May 2010 11:07:46 +0200 |
hoelzl |
added NEWS entry
|
changeset |
files
|
| Tue, 11 May 2010 19:19:45 +0200 |
hoelzl |
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
|
changeset |
files
|
| Tue, 11 May 2010 19:21:39 +0200 |
hoelzl |
Add rules directly to the corresponding class locales instead.
|
changeset |
files
|
| Tue, 11 May 2010 19:21:05 +0200 |
hoelzl |
Removed usage of normalizating locales.
|
changeset |
files
|
| Tue, 11 May 2010 21:55:41 -0700 |
huffman |
speed up some proofs, fixing linarith_split_limit warnings
|
changeset |
files
|
| Tue, 11 May 2010 19:38:16 -0700 |
huffman |
fix some linarith_split_limit warnings
|
changeset |
files
|
| Tue, 11 May 2010 19:01:35 -0700 |
huffman |
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
|
changeset |
files
|
| Tue, 11 May 2010 19:00:32 -0700 |
huffman |
fix duplicate simp rule warning
|
changeset |
files
|
| Tue, 11 May 2010 18:06:58 -0700 |
huffman |
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
|
changeset |
files
|
| Tue, 11 May 2010 17:20:11 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 11 May 2010 12:38:07 -0700 |
huffman |
simplify code for emptiness check
|
changeset |
files
|
| Tue, 11 May 2010 12:05:19 -0700 |
huffman |
removed lemma real_sq_order; use power2_le_imp_le instead
|
changeset |
files
|
| Tue, 11 May 2010 21:27:09 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 11 May 2010 19:06:18 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 11 May 2010 19:00:16 +0200 |
haftmann |
represent de-Bruin indices simply by position in list
|
changeset |
files
|
| Tue, 11 May 2010 18:46:03 +0200 |
haftmann |
tuned reification functions
|
changeset |
files
|
| Tue, 11 May 2010 18:31:36 +0200 |
haftmann |
tuned code; toward a tightended interface with generated code
|
changeset |
files
|