isabelle: Graph

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

datatype num = One | Dig0 num | Dig1 num
2009-02-16, by huffman
replace 1::num with One; remove monoid_mult instance
2009-02-16, by huffman
replace dec with double-and-decrement function
2009-02-15, by huffman
more default simp rules for sgn
2009-02-16, by haftmann
re-generated
2009-02-16, by haftmann
clarified import
2009-02-16, by haftmann
faster preprocessor
2009-02-16, by haftmann
added pdivmod on int (for code generation)
2009-02-16, by haftmann
merged
2009-02-16, by haftmann
tuned texts
2009-02-16, by haftmann
dropped Id
2009-02-16, by haftmann
dropped clause_suc_preproc for generic code generator
2009-02-16, by haftmann
new primrec
2009-02-16, by haftmann
Adapted to encoding of sets as predicates.
2009-02-16, by berghofe
enable auto-solve by default
2009-02-16, by kleing
merged
2009-02-16, by blanchet
Added nitpick attribute, and fixed typo.
2009-02-16, by blanchet
Added myself to testing list.
2009-02-16, by blanchet
dvd and setprod lemmas
2009-02-15, by nipkow
merged
2009-02-15, by nipkow
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