Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
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
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-01-13, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-01-09, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-19, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-15, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-11, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-10, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-10, by paulson
Updated comments.
2008-12-05, by paulson
dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
2009-01-29, by chaieb
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
2009-01-28, by chaieb
merged
2009-01-29, by nipkow
commented out unused lemmas. May need to be put back by Brian.
2009-01-29, by nipkow
-
2009-01-28, by nipkow
removed spurious conflic msg
2009-01-28, by nipkow
merged
2009-01-28, by nipkow
merged - resolving conflics
2009-01-28, by nipkow
Replaced group_ and ring_simps by algebra_simps;
2009-01-28, by nipkow
merged
2009-01-28, by haftmann
explicit check for exactly one type variable in class specification elements
2009-01-28, by haftmann
merged
2009-01-28, by huffman
merged
2009-01-27, by huffman
removed use of prev_cont_thms reference
2009-01-22, by huffman
merged
2009-01-22, by huffman
add lemmas about div/mod with multiplication
2009-01-21, by huffman
add lemmas about smult
2009-01-21, by huffman
merged
2009-01-28, by haftmann
slightly adapted towards more uniformity with div/mod on nat
2009-01-28, by haftmann
merged
2009-01-28, by haftmann
Plain, Main form meeting points in import hierarchy
2009-01-28, by haftmann
Plain, Main form meeting points in import hierarchy
2009-01-28, by haftmann
added lemma abs_sng
2009-01-28, by haftmann
nat is a bot instance
2009-01-28, by haftmann
slightly adapted towards more uniformity with div/mod on nat
2009-01-28, by haftmann
Reflection.thy now in HOL/Library
2009-01-28, by haftmann
more robust treatment of SwingUtilities.isEventDispatchThread;
2009-01-28, by wenzelm
annotate shared vars as @volatile;
2009-01-28, by wenzelm
updated generated file;
2009-01-27, by wenzelm
added label;
2009-01-27, by wenzelm
plain non-dependent types;
2009-01-27, by wenzelm
turned IsarDocument into trait for IsabelleProcess;
2009-01-27, by wenzelm
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
2009-01-27, by wenzelm
thm_proof: recovered single-threaded version;
2009-01-27, by wenzelm
merged
2009-01-27, by wenzelm
recovered example types from WordMain.thy;
2009-01-27, by wenzelm
merged
2009-01-27, by wenzelm
added share_common_data -- reduces heap space, but takes long;
2009-01-27, by wenzelm
use https;
2009-01-27, by wenzelm
thm_proof: replaced lazy by composed futures;
2009-01-27, by wenzelm
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2009-01-27, by wenzelm
explicit constraints
2009-01-26, by haftmann
entry point for Word library now named Word
2009-01-26, by haftmann
fixed reading of class specs: declare class operations in context
2009-01-26, by haftmann
stripped Id
2009-01-26, by haftmann
streamlined definitions, executable equality
2009-01-26, by haftmann
tuned header
2009-01-26, by haftmann
entry point for Word library now named Word
2009-01-26, by haftmann
correct proof of assm_intro rule
2009-01-26, by haftmann
sorted_take, sorted_drop
2009-01-26, by haftmann
merged
2009-01-23, by haftmann
fixed fixme
2009-01-23, by haftmann
avoiding misleading name duplicate
2009-01-23, by haftmann
lemmas dom_const, dom_if
2009-01-23, by haftmann
merged
2009-01-23, by wenzelm
moved all output to watcher-thread
2009-01-23, by immler
be more liberal with selected code statements
2009-01-23, by haftmann
making SMLNJ happy
2009-01-23, by haftmann
tuned signature;
2009-01-22, by wenzelm
binding replaces Binding.T
2009-01-22, by haftmann
binding replaces bstring
2009-01-22, by haftmann
simplified handling of base sort, dropped axclass
2009-01-22, by haftmann
dropped print_interps
2009-01-22, by haftmann
binding replaces bstring
2009-01-22, by haftmann
merged
2009-01-21, by haftmann
allow empty class specs
2009-01-21, by haftmann
changed import hierarchy
2009-01-21, by haftmann
no base sort in class import
2009-01-21, by haftmann
updated generated files;
2009-01-21, by wenzelm
removed Ids;
2009-01-21, by wenzelm
eliminated obsolete var morphism;
2009-01-21, by wenzelm
eliminated obsolete var morphism;
2009-01-21, by wenzelm
eliminated obsolete var morphism;
2009-01-21, by wenzelm
merged
2009-01-21, by wenzelm
tuned whitespace;
2009-01-21, by wenzelm
merged
2009-01-21, by wenzelm
removed vampire-wrapper (remote-script covers that)
2009-01-21, by immler
2 provers
2009-01-21, by immler
tuned;
2009-01-21, by immler
do not interrupt successful thread
2009-01-20, by immler
cancel whole group
2009-01-20, by immler
Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip
2009-01-20, by immler
pass timeout to prover;
2009-01-20, by immler
typo
2009-01-20, by immler
merged
2009-01-20, by immler
modified remote script;
2009-01-20, by immler
Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip
2009-01-19, by immler
removed useless
2009-01-14, by immler
simplified usage of remote-script; added compatible remote-atps
2009-01-12, by immler
dropped print_interps
2009-01-21, by haftmann
binding replaces bstring
2009-01-21, by haftmann
merged
2009-01-21, by haftmann
merged
2009-01-21, by haftmann
binding replaces bstring
2009-01-21, by haftmann
binding is alias for Binding.T
2009-01-21, by haftmann
dropped ID
2009-01-21, by haftmann
binding replaces bstring
2009-01-21, by haftmann
refined witness algebra
2009-01-21, by haftmann
code cleanup
2009-01-21, by haftmann
wrecked old locale package and related modules
2009-01-21, by haftmann
improved and corrected reading of class specs -- still draft version
2009-01-21, by haftmann
tuned
2009-01-21, by haftmann
tuned;
2009-01-20, by wenzelm
replaced java.util.Properties by plain association list;
2009-01-20, by wenzelm
replaced java.util.Properties by plain association list;
2009-01-20, by wenzelm
IsabelleSystem: provide Symbol.Interpretation;
2009-01-20, by wenzelm
more general init of Symbol.Interpretation, independent of IsabelleSystem instance;
2009-01-20, by wenzelm
more robust handling of quick_and_dirty;
2009-01-19, by wenzelm
Merged, overriding earlier fix.
2009-01-19, by ballarin
Fixed tutorial to compile with new locales; grammar of new locale commands.
2009-01-19, by ballarin
removed Ids;
2009-01-19, by wenzelm
removed Ids;
2009-01-19, by wenzelm
intern names of elements and attributes;
2009-01-19, by wenzelm
merged
2009-01-19, by haftmann
lcp = paulson
2009-01-19, by haftmann
"code equation" replaces "defining equation"
2009-01-19, by haftmann
tuned
2009-01-19, by haftmann
improved tackling of subclasses
2009-01-19, by haftmann
tuned proof
2009-01-19, by haftmann
smart path detection
2009-01-18, by haftmann
corrected user aliases
2009-01-18, by haftmann
added churn script
2009-01-18, by haftmann
Scala wrapper for interactive Isar documents;
2009-01-18, by wenzelm
added append_list, encode_list;
2009-01-18, by wenzelm
join_results: when dependencies are resulved (but not finished yet),
2009-01-18, by wenzelm
with_attributes: make double sure that unsafe attributes are avoided;
2009-01-18, by wenzelm
bug fixes
2009-01-18, by nipkow
bug fixes
2009-01-18, by nipkow
improved calculation of morphisms and rules
2009-01-18, by haftmann
merged
2009-01-17, by haftmann
tuned signature
2009-01-17, by haftmann
exported depedencies; tuned signature
2009-01-17, by haftmann
merged
2009-01-17, by huffman
merged
2009-01-16, by huffman
use match_tac instead of resolve_tac for continuity simproc
2009-01-15, by huffman
more instance declarations for poly
2009-01-15, by huffman
add lemmas about degree
2009-01-15, by huffman
rename plength to psize
2009-01-15, by huffman
rename divmod_poly to pdivmod
2009-01-15, by huffman
merged.
2009-01-15, by huffman
add strictness and compactness lemmas to Product_Cpo.thy
2009-01-15, by huffman
rename Dsum.thy to Sum_Cpo.thy
2009-01-14, by huffman
minimize dependencies
2009-01-14, by huffman
add lemmas cont2monofunE, cont2cont_apply
2009-01-14, by huffman
add Product_Cpo.thy
2009-01-14, by huffman
change to simpler, more extensible continuity simproc
2009-01-14, by huffman
merged
2009-01-17, by nipkow
bug fix
2009-01-17, by nipkow
merged
2009-01-17, by haftmann
code cleanup
2009-01-17, by haftmann
explicit equation morphism
2009-01-17, by haftmann
close derivation of classrels
2009-01-17, by haftmann
no document for HOL-Base
2009-01-17, by haftmann
moved message markup into Scala layer -- reduced redundancy;
2009-01-16, by wenzelm
added parse_body_failsafe;
2009-01-16, by wenzelm
define_state: use empty_state;
2009-01-16, by wenzelm
provide end_document;
2009-01-16, by wenzelm
merged
2009-01-16, by wenzelm
run command: check theory name for init;
2009-01-16, by wenzelm
run_command: check theory name for init;
2009-01-16, by wenzelm
export check_name;
2009-01-16, by wenzelm
fixed location of Imperative_HOL
2009-01-16, by haftmann
adapted to changes in class package
2009-01-16, by haftmann
merged
2009-01-16, by haftmann
migrated class package to new locale implementation
2009-01-16, by haftmann
corrected preparation of instances: parameters are proper names, not raw terms
2009-01-16, by haftmann
migrated class package to new locale implementation
2009-01-16, by haftmann
merged
2009-01-16, by wenzelm
fold_entries: non-optional start, permissive;
2009-01-16, by wenzelm
Result.toString: XML output of status messages;
2009-01-15, by wenzelm
added HOL-Base image
2009-01-16, by haftmann
moved Univ_Poly to Library
2009-01-16, by haftmann
merged
2009-01-16, by haftmann
tuned
2009-01-16, by haftmann
added cert_read_declaration; more exports; tuned signature
2009-01-16, by haftmann
merged
2009-01-15, by wenzelm
command 'Isar.edit_document': actually invoke edit_document;
2009-01-15, by wenzelm
merged
2009-01-15, by haftmann
fixed error message spacing
2009-01-15, by haftmann
tuned interpretation code
2009-01-15, by haftmann
tuned
2009-01-15, by haftmann
type constraints and sort intersection
2009-01-15, by haftmann
dropped $Id$
2009-01-15, by haftmann
decativate Toplevel.debug after reading
2009-01-15, by haftmann
exported break reference
2009-01-15, by Christian Urban
tuned;
2009-01-15, by wenzelm
edit_document: proper edits/edit markup, including the document id;
2009-01-15, by wenzelm
replaced command_state by edits/edit;
2009-01-15, by wenzelm
removed junk;
2009-01-15, by wenzelm
merged
2009-01-15, by wenzelm
one more [code del] declaration
2009-01-14, by huffman
misc cleanup and simplification;
2009-01-15, by wenzelm
added run_command (from isar_document.ML);
2009-01-15, by wenzelm
added command_state markup;
2009-01-15, by wenzelm
tuned ASCII art;
2009-01-14, by wenzelm
declare pCons_0_0 [code post]
2009-01-13, by huffman
merged
2009-01-13, by huffman
code generation for polynomials
2009-01-13, by huffman
merged
2009-01-13, by wenzelm
more [code del] declarations
2009-01-13, by huffman
declare more definitions [code del]
2009-01-13, by huffman
define polynomial multiplication using poly_rec
2009-01-13, by huffman
merged.
2009-01-13, by huffman
declare smult rules [simp]
2009-01-13, by huffman
simplify proof of coeff_mult_degree_sum
2009-01-13, by huffman
convert Deriv.thy to use new Polynomial library (incomplete)
2009-01-13, by huffman
Integration imports ATP_Linkup (for metis)
2009-01-13, by huffman
misc internal rearrangements;
2009-01-13, by wenzelm
replaced sys_error by plain error;
2009-01-13, by wenzelm
merged
2009-01-13, by wenzelm
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
2009-01-12, by huffman
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
2009-01-12, by huffman
add Polynomial.thy to makefile
2009-01-12, by huffman
add lemmas poly_power, poly_roots_finite
2009-01-12, by huffman
declare dvd_minus_iff and minus_dvd_iff [iff]
2009-01-12, by huffman
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
2009-01-12, by huffman
added Isar/isar_document.ML: Interactive Isar documents.
2009-01-13, by wenzelm
export list;
2009-01-13, by wenzelm
correctness and uniqueness of synthetic division
2009-01-12, by huffman
add synthetic division algorithm for polynomials
2009-01-12, by huffman
add list-style syntax for pCons
2009-01-12, by huffman
add recursion combinator poly_rec; define poly function using poly_rec
2009-01-12, by huffman
add lemmas degree_{add,diff}_less
2009-01-12, by huffman
merged
2009-01-11, by wenzelm
new theory of polynomials
2009-01-11, by huffman
tuned categories;
2009-01-11, by wenzelm
added outer_keyword.scala: Isar command keyword classification;
2009-01-11, by wenzelm
added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-11, by wenzelm
load main entry points sequentially, for reduced memory demands;
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
merged
2009-01-11, by haftmann
explicit bookkeeping of intro rules and axiom
2009-01-11, by haftmann
stripped Id
2009-01-11, by haftmann
construct explicit class morphism
2009-01-11, by haftmann
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
2009-01-10, by wenzelm
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
2009-01-10, by wenzelm
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10, by wenzelm
remove_thy: perform PureThy.cancel_proofs;
2009-01-10, by wenzelm
added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10, by wenzelm
added pending_groups -- accumulates task groups of local derivations only;
2009-01-10, by wenzelm
added cancel_group;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
schedule_futures: tuned final consolidation, explicit after_load phase;
2009-01-10, by wenzelm
load_thy: explicit after_load phase for presentation;
2009-01-10, by wenzelm
excursion: commit_exit internally -- checkpoints are fully persistent now;
2009-01-10, by wenzelm
slightly more robust matching of session name;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
fixed proof involving dvd;
2009-01-10, by wenzelm
tuned;
2009-01-10, by wenzelm
added force_result;
2009-01-10, by wenzelm
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
2009-01-10, by wenzelm
simplified join_proofs;
2009-01-10, by wenzelm
merged
2009-01-09, by wenzelm
added split_thy_path;
2009-01-09, by wenzelm
added running task markup;
2009-01-09, by wenzelm
tuned;
2009-01-08, by wenzelm
merged
2009-01-08, by wenzelm
merged
2009-01-09, by wenzelm
merged.
2009-01-09, by huffman
fix proof broken by changes in dvd theory
2009-01-09, by huffman
merged.
2009-01-08, by huffman
remove type-specific proofs
2009-01-08, by huffman
add lemma dvd_diff to class comm_ring_1
2009-01-08, by huffman
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
2009-01-08, by huffman
move lemmas mult_minus{left,right} inside class ring
2009-01-08, by huffman
clean up division_ring proofs
2009-01-08, by huffman
add class ring_div; generalize mod/diff/minus proofs for class ring_div
2009-01-08, by huffman
generalize zmod_zmod_cancel -> mod_mod_cancel
2009-01-08, by huffman
generalize some div/mod lemmas; remove type-specific proofs
2009-01-08, by huffman
add tracing for domain package proofs
2009-01-07, by huffman
rename abbreviation square -> power2, to match theorem names
2009-01-06, by huffman
merged
2009-01-09, by haftmann
split of Imperative_HOL theories from HOL-Library
2009-01-08, by haftmann
NEWS and CONTRIBUTORS
2009-01-08, by haftmann
dded code_thm antiquotation
2009-01-08, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip