Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
added finite_set_choice
2009-02-15, by nipkow
reject defined function in patterns with errmsg, e.g. f (f x) = x
2009-02-15, by krauss
fixed document
2009-02-15, by nipkow
more finiteness
2009-02-15, by nipkow
merged
2009-02-15, by nipkow
more finiteness
2009-02-15, by nipkow
merged
2009-02-14, by nipkow
more finiteness
2009-02-14, by nipkow
generalize lemma fps_square_eq_iff, move to Ring_and_Field
2009-02-14, by huffman
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
2009-02-14, by huffman
add mult_delta lemmas; simplify some proofs
2009-02-14, by huffman
fix spelling
2009-02-14, by huffman
declare fps_nth as a typedef morphism; clean up instance proofs
2009-02-14, by huffman
add lemma surj_from_nat
2009-02-14, by huffman
fix document generation
2009-02-14, by huffman
merged
2009-02-14, by huffman
fix document generation
2009-02-14, by huffman
section -> subsection
2009-02-13, by huffman
add instance for cancel_comm_monoid_add
2009-02-13, by huffman
add class cancel_comm_monoid_add
2009-02-13, by huffman
more finiteness changes
2009-02-14, by nipkow
merged
2009-02-13, by nipkow
finiteness lemmas
2009-02-13, by nipkow
merged
2009-02-13, by huffman
unset execute bit
2009-02-13, by huffman
Tuned datatype antiquotation.
2009-02-13, by berghofe
made SMLNJ happy
2009-02-13, by haftmann
typo
2009-02-13, by kleing
find_consts: display the search criteria. (by Timothy Bourke)
2009-02-13, by kleing
find_consts: documentation. (by Timothy Bourke)
2009-02-13, by kleing
FindTheorems solves: update documentation (by Timothy Bourke)
2009-02-13, by kleing
fixed codegen tool
2009-02-13, by haftmann
merged
2009-02-13, by haftmann
fixed codegen tool
2009-02-13, by haftmann
merged
2009-02-13, by nipkow
Moved Nat_Int_Bij into Library
2009-02-13, by nipkow
removed Reflection session
2009-02-13, by haftmann
add lemma add_nonneg_eq_0_iff
2009-02-12, by huffman
add lemmas about sgn
2009-02-12, by huffman
added ML file for the find_consts command
2009-02-13, by kleing
added find_consts to NEWS and CONTRIBUTORS
2009-02-13, by kleing
New command find_consts searching for constants by type (by Timothy Bourke).
2009-02-13, by kleing
fix document generation
2009-02-12, by huffman
move countability proof from Rational to Countable; add instance rat :: countable
2009-02-12, by huffman
Moved FTA into Lib and cleaned it up a little.
2009-02-12, by nipkow
ordered_idom instance for polynomials
2009-02-11, by huffman
Export tactic interface for sizechange method
2009-02-11, by krauss
merged
2009-02-11, by haftmann
liberal inst_meet
2009-02-11, by haftmann
display code theorems with HOL equality
2009-02-11, by haftmann
merged
2009-02-11, by blanchet
Added serial_string to SAT solver input and output files, to prevent multithreading chaos.
2009-02-10, by blanchet
Added nitpick_const_simp attribute to recdef and record packages.
2009-02-10, by blanchet
Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
2009-02-10, by blanchet
Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
2009-02-10, by blanchet
Reintroduced nitpick_ind_intro attribute.
2009-02-09, by blanchet
merged
2009-02-09, by blanchet
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
2009-02-09, by blanchet
merged
2009-02-06, by blanchet
Merged.
2009-02-06, by blanchet
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
2009-02-06, by blanchet
fixed typo
2009-02-11, by kleing
updated NEWS etc with "solves" criterion and auto_solves
2009-02-11, by kleing
merged
2009-02-11, by nipkow
Moved Order_Relation into Library and moved some of it into Relation.
2009-02-11, by nipkow
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-02-11, by kleing
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-02-11, by kleing
const_name antiquotations
2009-02-10, by huffman
Repaired a proof that did, after all, refer to the theorem nat_induct2.
2009-02-10, by paulson
merged
2009-02-10, by paulson
Strengthened the induction rule nat_induct2.
2009-02-10, by paulson
Deleted the induction rule nat_induct2, which was too weak and not used even once.
2009-02-10, by paulson
merged
2009-02-09, by nipkow
fix to [arith]
2009-02-09, by nipkow
new attribute "arith" for facts supplied to arith.
2009-02-09, by nipkow
Nicer names in FindTheorems.
2009-02-09, by Timothy Bourke
added Determinants to Library
2009-02-09, by chaieb
Traces, Determinant of square matrices and some properties
2009-02-09, by chaieb
added Euclidean_Space and Glbs to Library
2009-02-09, by chaieb
fixed proof -- removed unnecessary sorry
2009-02-09, by chaieb
Fixed theorem reference
2009-02-09, by chaieb
(Real) Vectors in Euclidean space, and elementary linear algebra.
2009-02-09, by chaieb
A generic decision procedure for linear rea arithmetic and normed vector spaces
2009-02-09, by chaieb
Permutations, both general and specifically on finite sets.
2009-02-09, by chaieb
Imports Main in order to avoid the typerep problem
2009-02-09, by chaieb
A theory of greatest lower bounds
2009-02-09, by chaieb
Now imports Fact as suggested by Florian in order to avoid the typerep problem
2009-02-09, by chaieb
Added HOL/Library/Finite_Cartesian_Product.thy to Library
2009-02-09, by chaieb
A formalization of finite cartesian product types
2009-02-09, by chaieb
Proof method 'reify' is now reentrant.
2009-02-09, by hoelzl
added noatps
2009-02-08, by nipkow
check for destination directory, do not allocate it gratuitously
2009-02-07, by haftmann
Isar proof
2009-02-07, by haftmann
merged
2009-02-07, by haftmann
code theorems for nth, list_update
2009-02-07, by haftmann
added bulkload
2009-02-07, by haftmann
code theorems for nth, list_update
2009-02-07, by haftmann
added bulkload
2009-02-07, by haftmann
added Decision_Procs.thy
2009-02-07, by haftmann
merged
2009-02-06, by haftmann
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-06, by haftmann
authentic syntax for List.nth
2009-02-06, by haftmann
Merged.
2009-02-06, by berghofe
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
2009-02-06, by blanchet
Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-02-06, by chaieb
fixed import
2009-02-06, by chaieb
merged
2009-02-06, by haftmann
more robust failure in error situations
2009-02-06, by haftmann
mandatory prefix for index conversion operations
2009-02-06, by haftmann
added replace operation
2009-02-06, by haftmann
fixed dependencies : Theory Dense_Linear_Order moved to Library
2009-02-06, by chaieb
Theory Dense_Linear_Order moved to Library
2009-02-06, by chaieb
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
2009-02-06, by chaieb
Updated NEWS about approximation
2009-02-05, by hoelzl
merged
2009-02-05, by haftmann
split of already properly working part of Quickcheck infrastructure
2009-02-05, by haftmann
code attribute applied before user attributes
2009-02-05, by haftmann
moved Random.thy to Library
2009-02-05, by haftmann
Add approximation method
2009-02-05, by hoelzl
Added new Float theory and moved old Library/Float.thy to ComputeFloat
2009-02-05, by hoelzl
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2009-02-05, by hoelzl
Make some Refute functions public so I can use them in Nitpick,
2009-02-04, by blanchet
merged
2009-02-04, by chaieb
Now catch ERROR exception thrown by find and friends
2009-02-04, by chaieb
dropped Id
2009-02-04, by haftmann
proper datatype abstraction example
2009-02-04, by haftmann
handling type classes without parameters
2009-02-03, by haftmann
adjusted theory name
2009-02-03, by haftmann
merged
2009-02-03, by haftmann
added stub about datatype abstraction
2009-02-03, by haftmann
changed name space policy for Haskell includes
2009-02-03, by haftmann
merged Big0
2009-02-03, by haftmann
added ROOT.ML for Reflection session
2009-02-03, by haftmann
merged
2009-02-03, by haftmann
established session HOL-Reflection
2009-02-03, by haftmann
established session HOL-Reflection
2009-02-03, by haftmann
regenerated presburger code
2009-02-03, by haftmann
merged Big0
2009-02-03, by haftmann
merge
2009-02-03, by nipkow
changed default timeout
2009-02-03, by immler
merged
2009-02-03, by haftmann
dropped global Nil/Append interpretation
2009-02-03, by haftmann
small fixes; removed Id
2009-02-03, by krauss
mergesort example: recdef->fun, localized
2009-02-03, by krauss
declare "nat o abs" as default measure for int
2009-02-03, by krauss
repaired accidental commit
2009-02-03, by haftmann
result for Swing.now;
2009-02-22, by wenzelm
replaced \overline by \vec;
2009-02-21, by wenzelm
updated generated files;
2009-02-21, by wenzelm
tuned;
2009-02-21, by wenzelm
updated generated files;
2009-02-20, by wenzelm
removed junk;
2009-02-20, by wenzelm
improved section "Rule composition";
2009-02-20, by wenzelm
tuned;
2009-02-20, by wenzelm
improved section on "Hereditary Harrop Formulae";
2009-02-20, by wenzelm
more on object-level rules;
2009-02-19, by wenzelm
updated generated files;
2009-02-18, by wenzelm
tuned;
2009-02-18, by wenzelm
more on local theories;
2009-02-18, by wenzelm
some text on local theory specifications;
2009-02-17, by wenzelm
some more Isar macros;
2009-02-17, by wenzelm
updated genereted files;
2009-02-16, by wenzelm
minor tuning and typographic fixes;
2009-02-16, by wenzelm
tuned refs;
2009-02-16, by wenzelm
removed rudiments of glossary;
2009-02-16, by wenzelm
removed rudiments of glossary;
2009-02-16, by wenzelm
removed unused glossary macros;
2009-02-16, by wenzelm
updated generated files;
2009-02-16, by wenzelm
observe usual theory naming conventions;
2009-02-16, by wenzelm
updated generated files;
2009-02-16, by wenzelm
tuned;
2009-02-16, by wenzelm
modernized some theory names;
2009-02-16, by wenzelm
eliminated old 'axclass';
2009-02-16, by wenzelm
avoid redefinition of FIXES/ASSUMES/SHOWS macros;
2009-02-16, by wenzelm
removed obsolete .cvsignore files;
2009-02-16, by wenzelm
removed obsolete axclass manual and examples;
2009-02-16, by wenzelm
explicit section for old/outdated manuals, which are still informative to some extent;
2009-02-15, by wenzelm
updated generated files;
2009-02-15, by wenzelm
added introduction;
2009-02-15, by wenzelm
added label;
2009-02-15, by wenzelm
removed obsolete section "User interfaces";
2009-02-15, by wenzelm
tuned spacing;
2009-02-15, by wenzelm
tuned;
2009-02-15, by wenzelm
updated generated files;
2009-02-15, by wenzelm
tuned;
2009-02-15, by wenzelm
added Isar/VM mode transition diagram;
2009-02-14, by wenzelm
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
2009-02-14, by wenzelm
clean_string/clean_name: proper treatment of \<dash>;
2009-02-14, by wenzelm
misc tuning;
2009-02-13, by wenzelm
added section "Canonical reasoning patterns";
2009-02-12, by wenzelm
improved sorry/noproof markup;
2009-02-12, by wenzelm
tuned;
2009-02-12, by wenzelm
updated generated files;
2009-02-12, by wenzelm
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
2009-02-12, by wenzelm
more on Isar framework -- mostly from Trybulec Festschrift;
2009-02-11, by wenzelm
more refs;
2009-02-11, by wenzelm
some more Isar elements;
2009-02-11, by wenzelm
added "inference" entity;
2009-02-11, by wenzelm
some more macros;
2009-02-11, by wenzelm
proof/qed: optional methods;
2009-02-11, by wenzelm
tuned formal markup;
2009-02-11, by wenzelm
updated generated files;
2009-02-09, by wenzelm
added introductory examples;
2009-02-09, by wenzelm
set quick_and_dirty;
2009-02-09, by wenzelm
tuned chapter heading;
2009-02-09, by wenzelm
added parts;
2009-02-09, by wenzelm
updated generated files;
2009-02-09, by wenzelm
basic setup for chapter "The Isabelle/Isar Framework";
2009-02-09, by wenzelm
more refs;
2009-02-09, by wenzelm
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
2009-02-02, by wenzelm
export lexicographic_order_tac
2009-02-02, by krauss
fix potential incompleteness in SAT encoding
2009-02-02, by krauss
avoid name clash of generated modules and includes
2009-02-02, by haftmann
strict check for locale target
2009-02-02, by haftmann
fixed proposition slip
2009-02-02, by haftmann
added Mapping.thy to Library
2009-02-02, by haftmann
dropped Id
2009-02-02, by haftmann
updated type class section
2009-02-02, by haftmann
updated class documentation
2009-02-02, by haftmann
merged
2009-02-01, by haftmann
added State_Monad theory in session
2009-02-01, by haftmann
proper declared constants in class expressions
2009-02-01, by haftmann
merged
2009-01-31, by nipkow
added some simp rules
2009-01-31, by nipkow
fixed case
2009-01-30, by krauss
Fixed theory name
2009-01-30, by chaieb
Added Formal_Power_Series_Examples to HOL-ex image
2009-01-30, by chaieb
Some applications of formal power Series
2009-01-30, by chaieb
Added real related theorems from Fact.thy
2009-01-30, by chaieb
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
2009-01-30, by chaieb
moved upwards in thy graph, real related theorems moved to Transcendental.thy
2009-01-30, by chaieb
Enclosed name containing _'s in @{text ...} antiquotation to make document
2009-01-29, by berghofe
Added strong congruence rule for UN.
2009-01-29, by berghofe
Added abs_def attribute.
2009-01-29, by berghofe
removed definition of funpow , reusing that of Relation_Power
2009-01-29, by chaieb
Added Formal_Power_Series in imports
2009-01-29, by chaieb
A formalization of formal power series
2009-01-29, by chaieb
Inserted Formal_Power_Series.thy under Library
2009-01-29, by chaieb
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-01-29, by paulson
Minor reorganisation of the Skolemization code
2009-01-29, by paulson
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip