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

removal of abel_cancel from Real
2003-12-11, by paulson
combining Real/{RealArith0,real_arith}.ML
2003-12-10, by paulson
Moving some theorems from Real/RealArith0.ML
2003-12-10, by paulson
Isar: where attribute supports instantiation of type variables.
2003-12-10, by ballarin
New structure "partial_object" as common root for lattices and magmas.
2003-12-10, by ballarin
Isar: where attribute supports instantiation of type vars.
2003-12-10, by ballarin
re-organisation of Real/RealArith0.ML; more `Isar scripts
2003-12-07, by paulson
moreover and also do not reset facts any more
2003-12-06, by kleing
do not reset facts ('this') for moreover and also
2003-12-06, by kleing
make Pure first to avoid race conditions on multiprocessor machines
2003-12-06, by kleing
revert to 1.18, changed Distribution/lib/Tools/makeall instead
2003-12-06, by kleing
make Pure first to avoid race conditions on multi processor machines
2003-12-06, by kleing
Added lazy sequences and parser combinators for same.
2003-12-05, by skalberg
more field division lemmas transferred from Real to Ring_and_Field
2003-12-05, by paulson
stylistic changes
2003-12-05, by paulson
Converting more of the "real" development to Isar scripts
2003-12-05, by paulson
hide Push
2003-12-04, by nipkow
further simplifications of the integer development; converting more .ML files
2003-12-04, by paulson
Tidying of the integer development; towards removing the
2003-12-04, by paulson
Simplification of the development of Integers
2003-12-03, by paulson
More re-organising of numerical theorems
2003-12-02, by paulson
conversion of some Real theories to Isar scripts
2003-11-28, by paulson
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
2003-11-27, by paulson
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
2003-11-25, by paulson
conversion of integers to use Ring_and_Field;
2003-11-24, by paulson
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
2003-11-21, by paulson
conversion of Integ/Int_lemmas.ML to Isar script
2003-11-20, by paulson
including 0 ~= 1 in definition of Field
2003-11-20, by paulson
additions to Ring_and_Field
2003-11-19, by paulson
fixed a comment
2003-11-18, by paulson
new theorems for Rings
2003-11-18, by paulson
conversion of ML to Isar scripts
2003-11-18, by paulson
Improved error handling: add_primrec now prints out ill-formed equation
2003-11-18, by berghofe
Type inference bug in Isar attributes "where" and "of" fixed.
2003-11-14, by ballarin
tidied
2003-11-12, by paulson
Records:
2003-11-06, by schirmer
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
2003-11-06, by ballarin
fixed
2003-10-31, by kleing
set isatool usedir to verbose by default
2003-10-31, by kleing
Got rid of the structure "Int", which was obsolete and which obscured the
2003-10-30, by paulson
Inserted additional checks in functions dest_prem and add_prod_factors, to
2003-10-29, by berghofe
tidying
2003-10-29, by paulson
Tuned proof of choice_eq.
2003-10-29, by berghofe
*** empty log message ***
2003-10-29, by nipkow
added sydney unsw mirror. contact: me (gerwin.klein@nicta.com.au)
2003-10-24, by kleing
auto update
2003-10-22, by paulson
InductiveInvariant_examples illustrates advanced recursive function definitions
2003-10-22, by paulson
recursion
2003-10-22, by paulson
Added access to the mk_rews field (and friends).
2003-10-21, by skalberg
Prevent recdef from looping when the inductio rule is simplified
2003-10-17, by paulson
improved tracing
2003-10-17, by paulson
partial conversion to Isar scripts
2003-10-16, by paulson
improved presentation
2003-10-16, by paulson
line-breaks; rewording
2003-10-16, by paulson
partial conversion to Isar scripts
2003-10-16, by paulson
Fixed bug in mk_ind_def that caused the inductive definition package to
2003-10-15, by berghofe
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
2003-10-15, by kleing
allow \<^sub> in identifiers
2003-10-15, by kleing
included \<^sub> in the range of identifier chars
2003-10-15, by kleing
Fixed spelling error.
2003-10-13, by skalberg
Added overview page.
2003-10-10, by berghofe
Munich webserver is now atbroy1
2003-10-10, by berghofe
trivial
2003-10-10, by paulson
finalconsts
2003-10-10, by paulson
Made judgments automatically declared final.
2003-10-10, by skalberg
better presentation
2003-10-10, by paulson
Added info on the new 'finalconsts' command.
2003-10-09, by skalberg
Added support for making constants final, that is, ensuring that no
2003-10-09, by skalberg
Added axiomatic specifications (ax_specification).
2003-10-08, by skalberg
now accepts DOS and Mac line breaks
2003-10-08, by paulson
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
2003-10-08, by paulson
added a comment
2003-10-03, by paulson
removal of junk and improvement of the document
2003-10-02, by paulson
Fixed inefficiency in post_definition by adding weak case congruence
2003-10-01, by berghofe
Removed garbage accidentally left behind in file.
2003-09-30, by ballarin
Improvements to Isar/Locales: premises generated by "includes" elements
2003-09-30, by ballarin
Improvements to Isar/Locales: premises generated by "includes" elements
2003-09-30, by ballarin
Changed order of prems in finprod_cong. Slight speedup.
2003-09-30, by ballarin
Improvements wrt rule_tac.
2003-09-30, by ballarin
Improvements to Isar/Locales: premises generated by "includes" elements
2003-09-30, by ballarin
new reference
2003-09-26, by paulson
tweak
2003-09-26, by paulson
misc tidying
2003-09-26, by paulson
Conversion of all main protocols from "Shared" to "Public".
2003-09-26, by paulson
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
2003-09-26, by paulson
new example for the Isar version of the ZF manual
2003-09-24, by paulson
Fixed soundness bug.
2003-09-23, by skalberg
conversion of NSP_Bad to Isar script
2003-09-23, by paulson
case_tac tweak
2003-09-23, by paulson
some basic new lemmas
2003-09-23, by paulson
Removal of the Key_supply axiom (affects many possbility proofs) and minor
2003-09-23, by paulson
new session HOL-SET-Protocol
2003-09-23, by paulson
Modified merge_aux to prevent newer names from getting overwritten
2003-09-22, by berghofe
add_attribute now takes parser as argument.
2003-09-22, by berghofe
Added "del" attribute for deleting equations.
2003-09-22, by berghofe
Changed interface of add_attribute.
2003-09-22, by berghofe
Improved efficiency of code generated for functions int and nat.
2003-09-22, by berghofe
Improved efficiency of code generated for + and -
2003-09-22, by berghofe
Improved efficiency of code generated for < predicate on natural numbers.
2003-09-22, by berghofe
Mod due to new thm in Map.
2003-09-15, by nipkow
Fixed blunder in the setup of the classical reasoner wrt. the constant
2003-09-15, by skalberg
Added the constant "curry".
2003-09-15, by skalberg
*** empty log message ***
2003-09-15, by nipkow
Added new theorems
2003-09-14, by nipkow
Added a number of thms about map restriction.
2003-09-11, by nipkow
Tried to make parser a bit more standard-conforming.
2003-09-04, by berghofe
Changed no_vars such that it outputs list of illegal schematic variables.
2003-09-04, by berghofe
quantifier symbols
2003-09-04, by paulson
conversion of HOL/Auth/KerberosIV to new-style theory
2003-09-04, by paulson
new, separate specifications
2003-09-04, by paulson
Introduced new syntax for maplets x |-> y
2003-09-03, by nipkow
Corrections due to John Matthews
2003-09-01, by paulson
Makes interactive proof scripting recognize the show_all_types flag.
2003-08-31, by skalberg
Added 'ambiguity_is_error' flag, which, if set, makes the parser fail,
2003-08-31, by skalberg
Added show_all_types flag, such that all type information in the term
2003-08-29, by skalberg
Method rule_tac understands Isar contexts: documentation.
2003-08-29, by ballarin
Methods rule_tac etc support static (Isar) contexts.
2003-08-29, by ballarin
Removed the extended digits again.
2003-08-29, by skalberg
Fixed typos.
2003-08-28, by skalberg
Extended the notion of letter and digit, such that now one may use greek,
2003-08-28, by skalberg