Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+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.
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
2010-05-12, by boehmes
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-14, by wenzelm
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-13, by wenzelm
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-13, by wenzelm
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13, by wenzelm
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13, by wenzelm
unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13, by wenzelm
added Proofterm.get_name variants according to krauss/schropp;
2010-05-13, by wenzelm
conditional structure SingleAssignment;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
tuned proofs and fact and class names
2010-05-12, by haftmann
tuned fact collection names and some proofs
2010-05-12, by haftmann
grouped local statements
2010-05-12, by haftmann
tuned test problems
2010-05-12, by haftmann
merged
2010-05-12, by wenzelm
merged
2010-05-12, by nipkow
simplified proof
2010-05-12, by nipkow
modernized specifications;
2010-05-12, by wenzelm
updated/unified some legacy warnings;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
do not emit legacy_feature warnings here -- users have no chance to disable them;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm
removed some obsolete admin stuff;
2010-05-12, by wenzelm
check NEWS;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm
updated some version numbers;
2010-05-12, by wenzelm
minor tuning;
2010-05-12, by wenzelm
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
modernized specifications; tuned reification
2010-05-12, by haftmann
merged
2010-05-12, by haftmann
added lemmas concerning last, butlast, insort
2010-05-12, by haftmann
Remove RANGE_WARN
2010-05-12, by Cezary Kaliszyk
clarified NEWS entry
2010-05-12, by hoelzl
merged
2010-05-12, by hoelzl
added NEWS entry
2010-05-12, by hoelzl
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
2010-05-11, by hoelzl
Add rules directly to the corresponding class locales instead.
2010-05-11, by hoelzl
Removed usage of normalizating locales.
2010-05-11, by hoelzl
speed up some proofs, fixing linarith_split_limit warnings
2010-05-11, by huffman
fix some linarith_split_limit warnings
2010-05-11, by huffman
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
2010-05-11, by huffman
fix duplicate simp rule warning
2010-05-11, by huffman
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-11, by huffman
merged
2010-05-11, by huffman
simplify code for emptiness check
2010-05-11, by huffman
removed lemma real_sq_order; use power2_le_imp_le instead
2010-05-11, by huffman
merged
2010-05-11, by haftmann
merged
2010-05-11, by haftmann
represent de-Bruin indices simply by position in list
2010-05-11, by haftmann
tuned reification functions
2010-05-11, by haftmann
tuned code; toward a tightended interface with generated code
2010-05-11, by haftmann
fix spelling of 'superseded'
2010-05-11, by huffman
NEWS: removed theory PReal
2010-05-11, by huffman
collected NEWS updates for HOLCF
2010-05-11, by huffman
merged
2010-05-11, by huffman
move floor lemmas from RealPow.thy to RComplete.thy
2010-05-11, by huffman
add lemma tendsto_Complex
2010-05-11, by huffman
move some theorems from RealPow.thy to Transcendental.thy
2010-05-11, by huffman
add lemma power2_eq_1_iff; generalize some other lemmas
2010-05-11, by huffman
minimize imports
2010-05-10, by huffman
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
2010-05-10, by huffman
clarified Pretty.font_metrics;
2010-05-12, by wenzelm
format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
more precise pretty printing based on actual font metrics;
2010-05-11, by wenzelm
predefined spaces;
2010-05-11, by wenzelm
merged
2010-05-11, by wenzelm
support Isabelle plugin properties with defaults;
2010-05-11, by wenzelm
merged
2010-05-11, by Christian Urban
tuned proof so that no simplifier warning is printed
2010-05-11, by Christian Urban
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-11, by haftmann
merged
2010-05-11, by haftmann
tuned
2010-05-11, by haftmann
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-05-11, by haftmann
tuned; dropped strange myassoc2
2010-05-10, by haftmann
stylized COOPER exception
2010-05-10, by haftmann
simplified oracle
2010-05-10, by haftmann
shorten names
2010-05-10, by haftmann
updated references to ML files
2010-05-10, by haftmann
only one module fpr presburger method
2010-05-10, by haftmann
moved int induction lemma to theory Int as int_bidirectional_induct
2010-05-10, by haftmann
tuned theory text; dropped unused lemma
2010-05-10, by haftmann
one structure is better than three
2010-05-10, by haftmann
less complex organization of cooper source code
2010-05-10, by haftmann
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
2010-05-10, by haftmann
add real_mult_commute to legacy theorem names
2010-05-10, by huffman
new construction of real numbers using Cauchy sequences
2010-05-10, by huffman
add more credits to ex/Dedekind_Real.thy
2010-05-10, by huffman
put construction of reals using Dedekind cuts in HOL/ex
2010-05-10, by huffman
disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
2010-05-11, by wenzelm
simple dialogs: ensure Swing thread;
2010-05-10, by wenzelm
font size re-adjustment according to Lobo internals;
2010-05-10, by wenzelm
Scala for Netbeans 6.8v1.1.0rc2;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-05-10, by wenzelm
more convenient look-and-feel setup;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;
2010-05-10, by wenzelm
updated to jedit 4.3.2;
2010-05-10, by wenzelm
ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
2010-05-10, by wenzelm
adapted to scala-2.8.0.RC2;
2010-05-10, by wenzelm
merged
2010-05-10, by wenzelm
real_mult_commute -> mult_commute
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
remove a couple of redundant lemmas; simplify some proofs
2010-05-09, by huffman
merged
2010-05-09, by huffman
add lemmas one_less_inverse and one_le_inverse
2010-05-08, by huffman
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
2010-05-09, by krauss
added lemmas rel_comp_UNION_distrib(2)
2010-05-09, by krauss
made SML/NJ happy;
2010-05-08, by wenzelm
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09, by wenzelm
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09, by wenzelm
just one version of Thm.unconstrainT, which affects all variables;
2010-05-09, by wenzelm
added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
2010-05-09, by wenzelm
tuned;
2010-05-09, by wenzelm
removed unused "option" variants of "same" operations;
2010-05-09, by wenzelm
more basic replacement of newlines;
2010-05-09, by wenzelm
static Symbol.spaces;
2010-05-09, by wenzelm
proper use of var stopped;
2010-05-08, by wenzelm
removed junk;
2010-05-08, by wenzelm
tuned headers;
2010-05-08, by wenzelm
tuned;
2010-05-08, by wenzelm
merged
2010-05-08, by wenzelm
merged
2010-05-08, by haftmann
moved normalization proof tool infrastructure to canonical algebraic classes
2010-05-08, by haftmann
added lemmas
2010-05-08, by nipkow
merged
2010-05-08, by haftmann
renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07, by haftmann
delete Groebner_Basis directory -- only one file left
2010-05-07, by haftmann
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-07, by haftmann
merged
2010-05-07, by haftmann
moved lemma zdvd_period to theory Int
2010-05-07, by haftmann
tuned;
2010-05-08, by wenzelm
discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08, by wenzelm
tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08, by wenzelm
unified/simplified Pretty.margin_default;
2010-05-08, by wenzelm
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-08, by wenzelm
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
2010-05-08, by wenzelm
tuned signature;
2010-05-08, by wenzelm
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08, by wenzelm
back-patching of axclass proofs;
2010-05-08, by wenzelm
back-patching via Single_Assignment.var;
2010-05-08, by wenzelm
support several sidekick parsers -- very basic default parser;
2010-05-07, by wenzelm
sidekick: unformatted content, notably without newlines;
2010-05-07, by wenzelm
unformatted output;
2010-05-07, by wenzelm
output symbolic pretty printing markup and format in the front end;
2010-05-07, by wenzelm
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
2010-05-07, by wenzelm
tuned;
2010-05-07, by wenzelm
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-07, by wenzelm
use existing undefined function;
2010-05-07, by wenzelm
merged
2010-05-07, by wenzelm
removed semicolons
2010-05-07, by krauss
rule subrelI (for nice Isar proofs of relation inequalities)
2010-05-07, by krauss
merged
2010-05-07, by wenzelm
merged
2010-05-07, by haftmann
prefix normalizing replaces class_semiring
2010-05-07, by haftmann
xsymbolized
2010-05-06, by haftmann
moved method syntax here
2010-05-06, by haftmann
tuned proof
2010-05-06, by haftmann
former free-floating field_comp_conv now in structure Normalizer
2010-05-06, by haftmann
proper sublocales; no free-floating ML sections
2010-05-06, by haftmann
moved some lemmas from Groebner_Basis here
2010-05-06, by haftmann
revert to loose merge semantics
2010-05-06, by haftmann
merged
2010-05-06, by haftmann
moved generic lemmas to appropriate places
2010-05-06, by haftmann
tuned
2010-05-06, by haftmann
dropped duplicate comp_arith
2010-05-06, by haftmann
avoid open; tuned references to theorems
2010-05-06, by haftmann
avoid references to groebner bases in names which have no references to groebner bases
2010-05-06, by haftmann
tuned whitespace
2010-05-06, by haftmann
tuned headings
2010-05-06, by haftmann
avoid open
2010-05-06, by haftmann
tuned internal structure
2010-05-06, by haftmann
fail on merge of conflicting normalization entries: functions are not mergable
2010-05-06, by haftmann
more canonical data administration
2010-05-06, by haftmann
removed former algebra presimpset entirely
2010-05-06, by haftmann
removed former algebra presimpset from accessor
2010-05-06, by haftmann
removed former algebra presimpset from signature
2010-05-06, by haftmann
moved presimplification rules for algebraic methods into named thms functor
2010-05-06, by haftmann
tuned whitespace; dropped superfluous open
2010-05-06, by haftmann
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-05-06, by haftmann
moved nat_arith ot Nat_Numeral: clarified normalizer setup
2010-05-05, by haftmann
dropped unused file
2010-05-05, by haftmann
dropped Id
2010-05-05, by haftmann
remove unused constant preal_of_rat; remove several unused lemmas about preals
2010-05-06, by huffman
respectfullness and preservation of prod_rel
2010-05-06, by Cezary Kaliszyk
ProofContext.init_global
2010-05-06, by haftmann
merged
2010-05-06, by haftmann
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-05, by haftmann
constant name access lattice is not in use any longer
2010-05-06, by haftmann
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
2010-05-06, by wenzelm
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06, by wenzelm
added separate;
2010-05-06, by wenzelm
basic formatting of pretty trees;
2010-05-06, by wenzelm
added content_length;
2010-05-06, by wenzelm
slightly more general Library.chunks;
2010-05-06, by wenzelm
misc tuning -- accumulate body via ListBuffer;
2010-05-06, by wenzelm
basic support for symbolic pretty printing;
2010-05-06, by wenzelm
extractors for document updates;
2010-05-06, by wenzelm
extractors for outer keyword declarations;
2010-05-06, by wenzelm
eliminated deprecated "--" method;
2010-05-05, by wenzelm
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
2010-05-05, by wenzelm
use SwingApplication instead of deprecated GUIApplication;
2010-05-05, by wenzelm
simplified via Position extractors;
2010-05-05, by wenzelm
some rearrangement of Scala sources;
2010-05-05, by wenzelm
fminus and some more theorems ported from Finite_Set.
2010-05-05, by Cezary Kaliszyk
eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05, by haftmann
tuned whitespace
2010-05-05, by haftmann
tuned interpunctation, dropped dead comment
2010-05-05, by haftmann
merged
2010-05-04, by huffman
avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)
2010-05-04, by huffman
generalize some lemmas to class t1_space
2010-05-04, by huffman
simplify definition of t1_space; generalize lemma closed_sing and related lemmas
2010-05-04, by huffman
generalize some lemmas
2010-05-04, by huffman
convert comments to 'text' blocks
2010-05-04, by huffman
generalize more lemmas about limits
2010-05-04, by huffman
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-05-05, by krauss
merged
2010-05-04, by huffman
generalize types of LIMSEQ and LIM; generalize many lemmas
2010-05-04, by huffman
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
2010-05-04, by huffman
make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-04, by huffman
adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
2010-05-04, by huffman
declare cont_discrete_cpo [cont2cont]
2010-05-04, by huffman
remove unneeded constant Zseq
2010-05-03, by huffman
add lemmas eventually_nhds_metric and tendsto_mono
2010-05-03, by huffman
remove unneeded premise
2010-05-03, by huffman
add constants netmap and nhds
2010-05-03, by huffman
Merged.
2010-05-04, by ballarin
Provide internal function for printing a single interpretation.
2010-05-04, by ballarin
Explicitly manage export in dependencies.
2010-04-27, by ballarin
fixed proof (cf. edc381bf7200);
2010-05-04, by wenzelm
Corrected imports; better approximation of dependencies.
2010-05-04, by hoelzl
Add Convex to Library build
2010-05-04, by hoelzl
Removed unnecessary assumption
2010-05-04, by hoelzl
Translating lemmas from Finite_Set to FSet.
2010-05-04, by Cezary Kaliszyk
merged
2010-05-04, by wenzelm
merged
2010-05-04, by berghofe
Turned Sem into an inductive definition.
2010-05-04, by berghofe
Corrected handling of "for" parameters.
2010-05-04, by berghofe
induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
2010-05-04, by berghofe
added lemma about irreflexivity of pointer inequality in Imperative_HOL
2010-05-04, by bulwahn
added function ffilter and some lemmas from Finite_Set to the FSet theory
2010-05-04, by bulwahn
merged
2010-05-04, by haftmann
avoid if on rhs of default simp rules
2010-05-04, by haftmann
avoid exception Empty on malformed goal
2010-05-04, by krauss
locale predicates of classes carry a mandatory "class" prefix
2010-05-04, by haftmann
a ring_div is a ring_1_no_zero_divisors
2010-05-04, by haftmann
NEWS
2010-05-04, by haftmann
merged
2010-05-03, by huffman
merged
2010-05-01, by huffman
complete_lattice instance for net type
2010-05-01, by huffman
swap ordering on nets, so x <= y means 'x is finer than y'
2010-05-01, by huffman
fixrec no longer uses global simpset internally to prove equations
2010-05-01, by huffman
move setsum lemmas to Product_plus.thy
2010-05-01, by huffman
remove duplicate lemmas
2010-04-30, by huffman
add lemmas about convergent
2010-04-30, by huffman
Cleanup information theory
2010-05-03, by hoelzl
Moved Convex theory to library.
2010-05-03, by hoelzl
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-20, by hoelzl
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04, by wenzelm
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04, by wenzelm
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-05-04, by wenzelm
specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result;
2010-05-04, by wenzelm
UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
2010-05-03, by wenzelm
replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
2010-05-03, by wenzelm
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03, by wenzelm
minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-05-03, by wenzelm
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
2010-05-03, by wenzelm
old NEWS on global operations;
2010-05-03, by wenzelm
ProofContext.init_global;
2010-05-03, by wenzelm
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-05-03, by wenzelm
merged
2010-05-03, by haftmann
do not generate code per default -- touches file of parent session
2010-04-30, by haftmann
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-05-01, by krauss
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
2010-05-01, by krauss
now if this doesn't make SML/NJ happy, nothing will
2010-05-01, by blanchet
more stats;
2010-05-01, by wenzelm
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-30, by wenzelm
slightly more standard induct_simp_add/del attributes;
2010-04-30, by wenzelm
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-30, by wenzelm
export Simplifier.with_context;
2010-04-30, by wenzelm
removed some old comments;
2010-04-30, by wenzelm
merged
2010-04-30, by huffman
merged
2010-04-30, by huffman
generalize lemma adjoint_unique; simplify some proofs
2010-04-29, by huffman
fix latex url
2010-04-29, by huffman
merged
2010-04-29, by huffman
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-29, by huffman
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0
2010-04-29, by huffman
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
2010-04-29, by huffman
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-04-29, by huffman
generalize LIMSEQ_vector to tendsto_vector
2010-04-28, by huffman
generalize orthogonal_clauses
2010-04-28, by huffman
remove redundant lemma vector_dist_norm
2010-04-28, by huffman
remove redundant lemma norm_0
2010-04-28, by huffman
generalize some euclidean space lemmas
2010-04-28, by huffman
prove lemma openin_subopen without using choice
2010-04-28, by huffman
move path-related stuff into new theory file
2010-04-28, by huffman
add new Multivariate_Analysis files to IsaMakefile
2010-04-28, by huffman
move operator norm stuff to new theory file
2010-04-28, by huffman
eliminated spurious sledgehammer invocation;
2010-04-30, by wenzelm
merged
2010-04-30, by wenzelm
merged
2010-04-30, by haftmann
merged
2010-04-30, by haftmann
enclose case expression in brackets
2010-04-30, by haftmann
catch the right exception
2010-04-30, by blanchet
eliminate trivial case splits from Isar proofs
2010-04-30, by blanchet
remove debugging code
2010-04-30, by blanchet
merged
2010-04-30, by blanchet
minor improvements
2010-04-30, by blanchet
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
2010-04-30, by blanchet
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
2010-04-30, by blanchet
in "overlord" mode: ignore problem prefix specified in the .thy file
2010-04-29, by blanchet
uncomment code
2010-04-29, by blanchet
redid some Sledgehammer/Metis proofs
2010-04-29, by blanchet
fix more "undeclared symbol" errors related to SPASS's DFG format
2010-04-29, by blanchet
be more discriminate: some one-line Isar proofs are silly
2010-04-29, by blanchet
one-step Isar proofs are not always pointless
2010-04-29, by blanchet
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
2010-04-29, by blanchet
redo more Metis/Sledgehammer example
2010-04-29, by blanchet
fixed definition of "bad frees" so that it actually works
2010-04-29, by blanchet
don't remove last line of proof
2010-04-29, by blanchet
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
2010-04-29, by blanchet
make SML/NJ happy, take 2
2010-04-29, by blanchet
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
2010-04-29, by blanchet
expand combinators in Isar proofs constructed by Sledgehammer;
2010-04-29, by blanchet
more neg_clausify proofs that get replaced by direct proofs
2010-04-29, by blanchet
redo some of the metis proofs
2010-04-28, by blanchet
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
2010-04-28, by blanchet
improve unskolemization
2010-04-28, by blanchet
make sure short theorem names are preferred to composite ones in Sledgehammer;
2010-04-28, by blanchet
properly extract SPASS proof
2010-04-28, by blanchet
try out Vampire 11 and parse its output correctly;
2010-04-28, by blanchet
return updated info record after termination proof
2010-04-30, by krauss
proper context for rule_by_tactic;
2010-04-30, by wenzelm
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
2010-04-30, by wenzelm
hgweb style: show author in filelog; full description in annotate hover
2010-04-29, by krauss
proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29, by wenzelm
read_const: disallow internal names as usual in visible Isar text;
2010-04-29, by wenzelm
more explicit treatment of context, although not fully localized;
2010-04-29, by wenzelm
removed some Emacs junk;
2010-04-29, by wenzelm
merged
2010-04-29, by haftmann
make random engine persistent using code_reflect
2010-04-29, by haftmann
repaired subtle misunderstanding: statement names are only passed for name resolution
2010-04-29, by haftmann
fixed underscore typo
2010-04-29, by haftmann
more coherent naming with ML serializer
2010-04-29, by haftmann
dropped code_datatype antiquotation
2010-04-29, by haftmann
dropped unnecessary ML code
2010-04-29, by haftmann
avoid popular infixes
2010-04-29, by haftmann
code_reflect: specify module name directly after keyword
2010-04-29, by haftmann
NEWS: code_reflect
2010-04-29, by haftmann
merged
2010-04-29, by haftmann
updated generated file
2010-04-28, by haftmann
modernized structure name
2010-04-28, by haftmann
use code_reflect
2010-04-28, by haftmann
merged
2010-04-29, by wenzelm
Tuning the quotient examples
2010-04-29, by Cezary Kaliszyk
clarified signature; simpler implementation in terms of function's tactic interface
2010-04-28, by krauss
return info record (relative to auxiliary context!)
2010-04-28, by krauss
default termination prover as plain tactic
2010-04-28, by krauss
function: sane interface for programmatic use
2010-04-28, by krauss
ML interface uses plain command names, following conventions from typedef
2010-04-28, by krauss
function: better separate Isar integration from actual functionality
2010-04-28, by krauss
merged
2010-04-29, by haftmann
export somehow odd mapa explicitly
2010-04-28, by haftmann
exported print_tuple
2010-04-28, by haftmann
take into account tupled constructors
2010-04-28, by haftmann
avoid code_datatype antiquotation
2010-04-28, by haftmann
merged
2010-04-28, by bulwahn
added an example with a free function variable to the Predicate Compile examples
2010-04-28, by bulwahn
removed local clone in the predicate compiler
2010-04-28, by bulwahn
improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
2010-04-28, by bulwahn
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
2010-04-29, by wenzelm
'write': actually observe the proof structure (like 'let' or 'fix');
2010-04-29, by wenzelm
adapted ProofContext.infer_type;
2010-04-29, by wenzelm
ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-29, by wenzelm
avoid clash with keyword 'write';
2010-04-29, by wenzelm
allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
2010-04-29, by wenzelm
uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
2010-04-29, by wenzelm
disabled spurious invocation of (interactive) sledgehammer;
2010-04-28, by wenzelm
merged
2010-04-28, by wenzelm
make Mirabelle happy
2010-04-28, by blanchet
remove removed option
2010-04-28, by blanchet
merge
2010-04-28, by blanchet
parentheses around nested cases
2010-04-28, by blanchet
merged
2010-04-28, by blanchet
add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
2010-04-28, by blanchet
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
2010-04-28, by blanchet
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
2010-04-28, by blanchet
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
2010-04-28, by blanchet
redo Sledgehammer proofs (and get rid of "neg_clausify")
2010-04-28, by blanchet
removed "sorts" option, continued
2010-04-28, by blanchet
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
2010-04-28, by blanchet
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
2010-04-28, by blanchet
support Vampire definitions of constants as "let" constructs in Isar proofs
2010-04-28, by blanchet
tuning
2010-04-27, by blanchet
redid the proofs with the latest Sledgehammer;
2010-04-27, by blanchet
remove Nitpick functions that are now implemented in Sledgehammer
2010-04-27, by blanchet
added total goal count as argument + message when killing ATPs
2010-04-27, by blanchet
make Sledgehammer more friendly if no subgoal is left
2010-04-27, by blanchet
polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs
2010-04-27, by blanchet
reintroduce missing "gen_all_vars" call
2010-04-27, by blanchet
fix types of "fix" variables to help proof reconstruction and aid readability
2010-04-27, by blanchet
allow schematic variables in types in terms that are reconstructed by Sledgehammer
2010-04-27, by blanchet
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
2010-04-27, by blanchet
new Isar proof construction code: stringfy axiom names correctly
2010-04-27, by blanchet
honor "shrink_proof" Sledgehammer option
2010-04-27, by blanchet
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-27, by blanchet
updated keywords
2010-04-28, by haftmann
exported cert_tyco, read_tyco
2010-04-28, by haftmann
added code_reflect command
2010-04-28, by haftmann
merged
2010-04-28, by haftmann
fix "fors" for proof of monotonicity
2010-04-28, by haftmann
merge
2010-04-28, by Cezary Kaliszyk
merge
2010-04-28, by Cezary Kaliszyk
Tuned FSet
2010-04-28, by Cezary Kaliszyk
merged
2010-04-28, by haftmann
try to observe intended meaning of add_registration interface more closely
2010-04-28, by haftmann
codified comment
2010-04-28, by haftmann
merged
2010-04-28, by haftmann
empty class specifcations observe default sort
2010-04-28, by haftmann
document some known problems with Mac OS;
2010-04-28, by wenzelm
removed redundant/ignored sort constraint;
2010-04-28, by wenzelm
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
2010-04-28, by wenzelm
made SML/NJ happy;
2010-04-28, by wenzelm
updated keywords;
2010-04-28, by wenzelm
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
2010-04-28, by wenzelm
removed material that is out of scope of this manual;
2010-04-28, by wenzelm
renamed command 'defaultsort' to 'default_sort';
2010-04-28, by wenzelm
localized default sort;
2010-04-28, by wenzelm
more systematic naming of tsig operations;
2010-04-28, by wenzelm
modernized/simplified Sign.set_defsort;
2010-04-28, by wenzelm
get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
2010-04-28, by wenzelm
export Type.minimize_sort;
2010-04-28, by wenzelm
term_typ: print styled term
2010-04-28, by haftmann
merged
2010-04-27, by wenzelm
merged
2010-04-27, by huffman
generalize types of path operations
2010-04-27, by huffman
generalize more continuity lemmas
2010-04-27, by huffman
generalized many lemmas about continuity
2010-04-27, by huffman
simplify definition of continuous_on; generalize some lemmas
2010-04-26, by huffman
move intervals section heading
2010-04-26, by huffman
remove unused, redundant constant inv_on
2010-04-26, by huffman
reorganize subsection headings
2010-04-26, by huffman
remove redundant lemma
2010-04-26, by huffman
more lemmas to Vec1.thy
2010-04-26, by huffman
simplify proof
2010-04-26, by huffman
move more lemmas into Vec1.thy
2010-04-26, by huffman
move proof of Fashoda meet theorem into separate file
2010-04-26, by huffman
move definitions and theorems for type real^1 to separate theory file
2010-04-26, by huffman
removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27, by wenzelm
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27, by wenzelm
really minimize sorts after certification -- looks like this is intended here;
2010-04-27, by wenzelm
tuned signature;
2010-04-27, by wenzelm
merged
2010-04-27, by wenzelm
tuned whitespace
2010-04-27, by haftmann
got rid of [simplified]
2010-04-27, by haftmann
got rid of [simplified]
2010-04-27, by haftmann
fix SML/NJ compilation (I hope)
2010-04-27, by blanchet
tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27, by wenzelm
tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27, by wenzelm
tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27, by wenzelm
clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27, by wenzelm
misc tuning and simplification;
2010-04-27, by wenzelm
NEWS and CONTRIBUTORS
2010-04-27, by haftmann
explicit is better than implicit
2010-04-27, by haftmann
tuned class linordered_field_inverse_zero
2010-04-27, by haftmann
merged
2010-04-27, by haftmann
instances for *_inverse_zero classes
2010-04-27, by haftmann
canonical import
2010-04-27, by haftmann
merged
2010-04-26, by haftmann
use new classes (linordered_)field_inverse_zero
2010-04-26, by haftmann
merged
2010-04-26, by blanchet
renamed option
2010-04-26, by blanchet
fixes 2a5c6e7b55cb;
2010-04-26, by blanchet
compile
2010-04-26, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip