isabelle: Graph

suppress document output
2009-03-07, by haftmann
theory with syntax for lattice operations
2009-03-06, by haftmann
added babel -- necessary for bind infix syntax
2009-03-06, by haftmann
added enumeration of predicates
2009-03-06, by haftmann
moved instance option :: finite to Option.thy
2009-03-06, by haftmann
constructive version of Cantor's first diagonalization argument
2009-03-06, by haftmann
equalities for Min, Max
2009-03-06, by haftmann
merged
2009-03-06, by wenzelm
added lemma
2009-03-06, by nipkow
merged
2009-03-06, by nipkow
Docs
2009-03-06, by nipkow
eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-06, by wenzelm
schedule_seq: handle after_load errors as in schedule_futures;
2009-03-06, by wenzelm
replaced archaic use of rep_ss by Simplifier.mksimps;
2009-03-06, by wenzelm
improved error handling for document antiquotations;
2009-03-06, by wenzelm
merged
2009-03-06, by blanchet
merged
2009-03-06, by nipkow
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
2009-03-06, by blanchet
added lemmas
2009-03-06, by nipkow
Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead.
2009-03-06, by blanchet
merged
2009-03-06, by blanchet
merged
2009-03-06, by blanchet
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
2009-03-06, by blanchet
merged
2009-03-06, by haftmann
merged
2009-03-06, by haftmann
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-06, by haftmann
merged
2009-03-05, by haftmann
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05, by haftmann
tuned
2009-03-05, by haftmann
moved complete_lattice to Set.thy
2009-03-05, by haftmann
dropped Id
2009-03-05, by haftmann
corrected slip in NEWS
2009-03-06, by haftmann
merged
2009-03-06, by haftmann
added strict_mono predicate
2009-03-06, by haftmann
Identifiers of some old CVS file versions;
2009-03-06, by wenzelm
recovered generated files;
2009-03-06, by wenzelm
more precise deps;
2009-03-06, by wenzelm
merged
2009-03-06, by nipkow
Added Docs
2009-03-06, by nipkow
render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
2009-03-05, by wenzelm
removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
2009-03-05, by wenzelm
removed unused TableFun().fold_map and GraphFun().fold_map_nodes;
2009-03-05, by wenzelm
removed spurious occurrences of old rep_ss;
2009-03-05, by wenzelm
Thm.add_oracle interface: replaced old bstring by binding;
2009-03-05, by wenzelm
silent chmod;
2009-03-05, by wenzelm
Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05, by wenzelm
close_schematic_term: uniform order of types/terms;
2009-03-05, by wenzelm
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05, by wenzelm
TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
2009-03-05, by wenzelm
fixed proofs -- follow-up to ecd6f0ca62ea;
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name");
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name;
2009-03-05, by wenzelm
eliminated obsolete ProofContext.full_bname;
2009-03-05, by wenzelm
Binding.prefix_of;
2009-03-05, by wenzelm
adapted Binding.dest;
2009-03-05, by wenzelm
added prefix_of;
2009-03-05, by wenzelm
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-05, by blanchet
merged
2009-03-05, by wenzelm
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04, by huffman
regenerated document;
2009-03-05, by wenzelm
merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
2009-03-05, by wenzelm
dummy changes to produce a new changeset of these files;
2009-03-05, by wenzelm
updated generated file -- changed since @{ML} now ignores source flag;
2009-03-05, by wenzelm
fixed document;
2009-03-05, by wenzelm
removed old/broken CVS Ids;
2009-03-04, by wenzelm
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
2009-03-04, by wenzelm
merged
2009-03-04, by chaieb
Moved general theorems about sums and products to FiniteSet.thy
2009-03-04, by chaieb
fixed proofs; added rules as default simp-rules
2009-03-04, by chaieb
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
2009-03-04, by chaieb
Added Libray dependency on Topology_Euclidean_Space
2009-03-04, by chaieb
Added general theorems for fold_image, setsum and set_prod
2009-03-04, by chaieb
fixed proofs
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-02-25, by chaieb
merged
2009-02-25, by chaieb
Second try at adding "nitpick_const_def" attribute.
2009-03-04, by blanchet
Fix parentheses.
2009-03-04, by blanchet
merged
2009-03-04, by blanchet
Added "nitpick_const_simp" attribute to Nominal primrec.
2009-03-04, by blanchet
NEWS: renamed o2s to Option.set;
2009-03-04, by wenzelm
less arbitrary occurrences of undefined
2009-03-04, by haftmann
datatype antiquotation does not assume LaTeX as output any longer
2009-03-04, by haftmann
merged
2009-03-04, by nipkow
Option.thy
2009-03-04, by nipkow
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
2009-03-04, by haftmann
merged
2009-03-04, by haftmann
explicit error message for `improper` instances lacking explicit instance parameter constants
2009-03-04, by haftmann
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Made Refute.norm_rhs public, so I can use it in Nitpick.
2009-03-04, by blanchet
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
2009-03-01, by blanchet
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
2009-02-24, by blanchet
merged
2009-03-04, by nipkow
Made Option a separate theory and renamed option_map to Option.map
2009-03-04, by nipkow
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-04, by wenzelm
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
2009-03-03, by wenzelm
tuned str_of, now subject to verbose flag;
2009-03-03, by wenzelm
added @{binding} ML antiquotations;
2009-03-03, by wenzelm
added print_properties, print_position (again);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
merged
2009-03-03, by haftmann
tuned manuals
2009-03-03, by haftmann
more canonical directory structure of manuals
2009-03-03, by haftmann
merged
2009-03-03, by wenzelm
removed and renamed redundant lemmas
2009-03-03, by nipkow
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03, by wenzelm
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
2009-03-03, by wenzelm
added markup for binding;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
renamed Binding.display to Binding.str_of, which is slightly more canonical;
2009-03-03, by wenzelm
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
2009-03-03, by wenzelm
moved name space externalization flags back to name_space.ML;
2009-03-03, by wenzelm
moved name space externalization flags back to name_space.ML;
2009-03-03, by wenzelm
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
Thm.binding;
2009-03-03, by wenzelm
added type binding and val empty_binding;
2009-03-03, by wenzelm
updated generated files;
2009-03-03, by wenzelm
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
2009-03-03, by wenzelm
Implement Makarius's suggestion for improved type pattern parsing.
2009-03-03, by Timothy Bourke
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
2009-03-02, by Timothy Bourke
adapted to lates experimental version;
2009-03-02, by wenzelm
removed Ids;
2009-03-02, by wenzelm
merged
2009-03-02, by haftmann
reduced confusion code_funcgr vs. code_wellsorted
2009-03-02, by haftmann
better markup
2009-03-02, by haftmann
name fix
2009-03-02, by nipkow
merged
2009-03-02, by nipkow
name changes
2009-03-02, by nipkow
Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-03-02, by chaieb
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
2009-03-02, by chaieb
fixed broken @{file} refs;
2009-03-02, by wenzelm
merged
2009-03-02, by wenzelm
using plain ISABELLE_PROCESS
2009-03-02, by haftmann
merged
2009-03-02, by haftmann
ignore ISABELLE_LINE_EDITOR for code generation
2009-03-02, by haftmann
use long names for old-style fold combinators;
2009-03-01, by wenzelm
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-03-01, by wenzelm
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
2009-03-01, by wenzelm
end_timing: generalized result -- message plus with explicit time values;
2009-03-01, by wenzelm
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
2009-03-01, by wenzelm
updated contributors;
2009-03-01, by wenzelm
removed parts of the manual that are clearly obsolete, or covered by
2009-03-01, by wenzelm
merged
2009-03-01, by wenzelm
minor update of Mercurial HOWTO;
2009-03-01, by wenzelm
removed redundant lemmas
2009-03-01, by nipkow
added lemmas by Jeremy Avigad
2009-03-01, by nipkow
A Serbian theory, by Filip Maric.
2009-02-28, by wenzelm
more accurate deps;
2009-02-28, by wenzelm
merged
2009-02-28, by wenzelm
add news for HOLCF; fixed some typos and inaccuracies
2009-02-28, by huffman
fixed headers;
2009-02-28, by wenzelm
moved isabelle_system.scala to src/Pure/System/;
2009-02-28, by wenzelm
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2009-02-28, by wenzelm
updated generated files;
2009-02-28, by wenzelm
added method "coherent";
2009-02-28, by wenzelm
more refs;
2009-02-28, by wenzelm
moved method "iprover" to HOL specific part;
2009-02-28, by wenzelm
removed Ids;
2009-02-28, by wenzelm
simultaneous use_thys;
2009-02-28, by wenzelm
replaced low-level 'no_syntax' by 'no_notation';
2009-02-28, by wenzelm
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28, by wenzelm
tuned message;
2009-02-28, by wenzelm
* New prover for coherent logic (see src/Tools/coherent.ML).
2009-02-28, by wenzelm
more CONTRIBUTORS;
2009-02-28, by wenzelm
removed Ids;
2009-02-28, by wenzelm
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-28, by wenzelm
some updates on ancient README;
2009-02-28, by wenzelm
fixrec package uses new-style syntax and local-theory interface
2009-02-27, by huffman
add function taken_names
2009-02-27, by huffman
merged
2009-02-27, by huffman
make list-style polynomial syntax work when show_sorts is on
2009-02-27, by huffman
more CONTRIBUTORS;
2009-02-27, by wenzelm
turned "read-only refs" typ_level and minimize_applies into constant values;
2009-02-27, by wenzelm
merged
2009-02-27, by wenzelm
removed global ref dfg_format
2009-02-26, by immler
removed local ref const_needs_hBOOL;
2009-02-25, by immler
removed local ref const_min_arity
2009-02-24, by immler
eliminated private clones of List.partition;
2009-02-27, by wenzelm
observe some Isabelle/ML coding conventions;
2009-02-27, by wenzelm
eliminated NJ's List.nth;
2009-02-27, by wenzelm
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
2009-02-27, by wenzelm
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
2009-02-27, by wenzelm
observe basic Isabelle/ML coding conventions;
2009-02-27, by wenzelm
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
2009-02-27, by wenzelm
added ML-Systems/polyml-experimental.ML;
2009-02-27, by wenzelm
tuned;
2009-02-27, by wenzelm
even less default memory for sunbroy2;
2009-02-27, by wenzelm
merged
2009-02-27, by boehmes
merged
2009-02-27, by boehmes
Made then_conv and else_conv available as infix operations.
2009-02-26, by boehmes
merged
2009-02-27, by haftmann
fixed typo
2009-02-27, by haftmann
merged
2009-02-26, by huffman
avoid using legacy type inference
2009-02-26, by huffman
use TheoryData to keep track of pattern match combinators
2009-02-26, by huffman
merged
2009-02-26, by huffman
remove unnecessary simp rules
2009-02-26, by huffman
revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
2009-02-26, by huffman
merged
2009-02-26, by wenzelm
back to canonical ROOT, to see if memory problems still persist;
2009-02-26, by wenzelm
trying less default memory for sunbroy2 test
2009-02-27, by kleing
basic setup for chapter "Syntax and type-checking";
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
standard headers;
2009-02-26, by wenzelm
updated generated files;
2009-02-26, by wenzelm
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
2009-02-26, by wenzelm
fixed import of ~~/src/HOL/Decision_Procs/Ferrack;
2009-02-26, by wenzelm
more explicit indication of old manuals;
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
\bibliographystyle{abbrv} for newer ref manuals;
2009-02-26, by wenzelm
added Haftmann-Wenzel:2009;
2009-02-26, by wenzelm
updated generated files;
2009-02-26, by wenzelm
isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
include HOL-Decision_Procs in stats;
2009-02-26, by wenzelm
back to plain http;
2009-02-26, by wenzelm
merged
2009-02-26, by berghofe
Added postprocessing rules for fresh_star.
2009-02-26, by berghofe
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
2009-02-26, by berghofe
tuned NEWS;
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
merged
2009-02-26, by huffman
add type annotation
2009-02-26, by huffman
disable floor_minus and ceiling_minus [simp]
2009-02-26, by huffman
merged
2009-02-26, by wenzelm
merged
2009-02-26, by paulson
Updated the theory syntax. Corrected an error in a command.
2009-02-26, by paulson
merged
2009-02-25, by huffman
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
2009-02-25, by huffman
new theory of Archimedean fields
2009-02-25, by huffman
add lemmas about comparisons of Fract a b with 0 and 1
2009-02-25, by huffman
merged
2009-02-25, by huffman
add lemma diff_Suc_1
2009-02-25, by huffman
Added lemmas for normalizing freshness results involving fresh_star.
2009-02-25, by berghofe
Added typing and evaluation relations, together with proofs of preservation
2009-02-25, by berghofe
merged
2009-02-25, by berghofe
Use LocalTheory.full_name instead of Sign.full_name, because the latter does
2009-02-25, by berghofe
Replaced Logic.unvarify by Variable.import_terms to make declaration of
2009-02-25, by berghofe
nominal_inductive and equivariance now work on local_theory.
2009-02-25, by berghofe
Added equivariance lemmas for fresh_star.
2009-02-25, by berghofe
NEWS
2009-02-25, by nipkow
merged
2009-02-25, by haftmann
robustified
2009-02-25, by haftmann
make more proofs work whether or not One_nat_def is a simp rule
2009-02-24, by huffman
add simp rules for numerals with 1::nat
2009-02-24, by huffman
fix lemma hypreal_hnorm_def
2009-02-24, by huffman
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-23, by huffman
move lemma dvd_mod_imp_dvd into class semiring_div
2009-02-23, by huffman
merged
2009-02-23, by haftmann
improved treatment of case certificates
2009-02-23, by haftmann
repaired order of variable node allocation
2009-02-23, by haftmann
explicitly import Fact
2009-02-23, by huffman
change imports to move Fact.thy outside Plain
2009-02-23, by huffman
add lemmas poly_{div,mod}_minus_{left,right}
2009-02-23, by huffman
merged
2009-02-23, by huffman
declare scaleR distrib rules [algebra_simps]; cleaned up
2009-02-22, by huffman
clean up instantiations
2009-02-22, by huffman
merged
2009-02-22, by huffman
simplify some proofs
2009-02-22, by huffman
remove duplicate instance declaration
2009-02-22, by huffman
stripped classrels_of, instances_of
2009-02-23, by haftmann
use canonical subalgebra projection
2009-02-23, by haftmann
experimental switch to new well-sorting algorithm
2009-02-22, by haftmann
handle NONE case in arity function properly
2009-02-22, by haftmann
clarified status of variables in evaluation terms; tuned header
2009-02-22, by haftmann
subalgebra: drop arities if desired
2009-02-22, by haftmann
merged
2009-02-22, by haftmann
more liberality needed
2009-02-22, by haftmann
merged
2009-02-22, by nipkow
added lemmas
2009-02-22, by nipkow
merged
2009-02-22, by haftmann
simplified evaluation
2009-02-22, by haftmann
merged
2009-02-22, by nipkow
added dvd_div_mult
2009-02-22, by nipkow
merged
2009-02-22, by haftmann
first attempt to solve evaluation bootstrap problem
2009-02-22, by haftmann
formal dependency on newly emerging algorithm
2009-02-22, by haftmann
merged
2009-02-22, by nipkow
name fix
2009-02-22, by nipkow
fix spelling
2009-02-21, by huffman
real_inner class instance for vectors
2009-02-21, by huffman
NEWS
2009-02-21, by nipkow
merged
2009-02-21, by nipkow
Removed subsumed lemmas
2009-02-21, by nipkow
remove duplicated lemmas about norm
2009-02-21, by huffman
real_normed_vector instance
2009-02-21, by huffman
fix real_vector, real_algebra instances
2009-02-21, by huffman
merged
2009-02-21, by huffman
generalize lemmas from nat to 'a::wellorder
2009-02-20, by huffman
generalize some lemmas
2009-02-20, by huffman
merged
2009-02-21, by nipkow
removed redundant thms
2009-02-21, by nipkow
merged
2009-02-20, by huffman
class instances for num1
2009-02-20, by huffman
Removed redundant lemmas
2009-02-20, by nipkow
merged
2009-02-20, by haftmann
also consider superclasses properly
2009-02-20, by haftmann
merged
2009-02-20, by nipkow
removed subsumed lemmas
2009-02-20, by nipkow
merged
2009-02-20, by haftmann
datatype antiquotation: always bracket types with spaces in between
2009-02-20, by haftmann
consequent use of term `code equation`
2009-02-20, by haftmann
permissive check for pattern discipline in case schemes
2009-02-20, by haftmann
maintain order of constructors in datatypes; clarified conventions for type schemes
2009-02-20, by haftmann
stripped Id
2009-02-20, by haftmann
merged
2009-02-20, by huffman
add theory of products as real vector spaces to Library
2009-02-20, by huffman
add new theory Product_plus.thy to Library
2009-02-20, by huffman
merged
2009-02-20, by immler
changed message
2009-02-20, by immler
detailed information on atp-failure via Output.debug
2009-02-20, by immler
merged
2009-02-20, by haftmann
reverted to old wellsorting algorithm
2009-02-20, by haftmann
fixed spurious proof failure
2009-02-20, by haftmann
consider changes variable names in theorem le_imp_power_dvd
2009-02-20, by haftmann
tuned and incremental version of wellsorting algorithm
2009-02-20, by haftmann
ignore sorts in bare types
2009-02-20, by haftmann
defensive implementation of pretty serialisation of lists and characters
2009-02-20, by haftmann
dropped Id
2009-02-20, by haftmann
experimental inclusion of new wellsorting algorithm for code equations
2009-02-20, by haftmann
merged
2009-02-20, by chaieb
merged
2009-02-17, by chaieb
merged
2009-02-17, by chaieb
fixed selection of premises
2009-02-17, by chaieb
cleaned up
2009-02-19, by huffman
declare of_int_number_of_eq [simp]
2009-02-19, by huffman
fix case_names
2009-02-19, by huffman
nicer induction/cases rules for numeral types
2009-02-19, by huffman
number_ring instances for numeral types
2009-02-19, by huffman
declare xor_compl_{left,right} [simp]
2009-02-19, by huffman
add rule for minus 1 at type bit
2009-02-19, by huffman
add formalization of a type of integers mod 2 to Library
2009-02-19, by huffman
new theory of real inner product spaces
2009-02-19, by huffman
add Powerdomain_ex.thy
2009-02-19, by huffman
add more ordering lemmas
2009-02-19, by huffman
avoid using ab_semigroup_idem_mult locale for powerdomains
2009-02-19, by huffman
merged
2009-02-19, by huffman
add header
2009-02-18, by huffman
move Polynomial.thy to Library
2009-02-18, by huffman
move FrechetDeriv.thy to Library
2009-02-18, by huffman
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-18, by huffman
half auto_solve default time out; increase manually in PG for large projects
2009-02-19, by kleing
merged
2009-02-18, by huffman
finish converting Deriv.thy to new polynomial library
2009-02-18, by huffman
generalize int_dvd_cancel_factor simproc to idom class
2009-02-18, by huffman
composition of polynomials
2009-02-18, by huffman
add some lemmas, cleaned up
2009-02-18, by huffman
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
2009-02-18, by huffman
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
2009-02-18, by huffman
merged
2009-02-18, by huffman
more subsection headings
2009-02-18, by huffman
speed up proof of exp_exists
2009-02-18, by huffman
tuned
2009-02-18, by haftmann
sort instances wrt. to class hierarchy
2009-02-18, by haftmann
fixed signature
2009-02-18, by haftmann
tuned accessor name
2009-02-18, by haftmann
more precise improvement in instantiation user space type system
2009-02-18, by haftmann
do not drop arguments to 0, 1
2009-02-18, by haftmann
merged
2009-02-18, by haftmann
reverted to previous version of Finite_Set.thy
2009-02-18, by haftmann
merged
2009-02-18, by haftmann
merged
2009-02-18, by haftmann
first working version
2009-02-18, by haftmann
tuned comments, stripped ID, deleted superfluous code
2009-02-18, by haftmann
stripped ID
2009-02-18, by haftmann
Syntactic support for products over set intervals
2009-02-18, by paulson
No idea what happened here!
2009-02-18, by paulson
Even and odd powers of -1
2009-02-17, by paulson
merged
2009-02-18, by blanchet
Reintroduce set_interpreter for Collect and op :.
2009-02-17, by blanchet
Added Nitpick tag to 'of_int_of_nat'.
2009-02-16, by blanchet
add lemmas for exponentiation
2009-02-17, by huffman
merged
2009-02-17, by haftmann
unified variable names in case expressions; no exponential fork in translation of case expressions
2009-02-17, by haftmann
merged
2009-02-17, by huffman
remove redundant simp attributes for zdvd rules
2009-02-17, by huffman
lemmas abs_dvd_iff, dvd_abs_iff
2009-02-17, by huffman
Cleaned up IntDiv and removed subsumed lemmas.
2009-02-17, by nipkow
tune section headings; add square function
2009-02-16, by huffman
merged
2009-02-16, by huffman
rearrange subsections
2009-02-16, by huffman
remove instances num::semiring and num::linorder
2009-02-16, by huffman
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