isabelle: Graph

tweaking of lemmas in RealDef, RealOrd
2004-01-01, by paulson
\<^bsub> .. \<^esub>
2003-12-29, by kleing
spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup>
2003-12-29, by kleing
re-organized numeric lemmas
2003-12-27, by paulson
Added trace msg
2003-12-25, by nipkow
re-organized some hyperreal and real lemmas
2003-12-25, by paulson
list_all2_nthD no good as [intro?]
2003-12-24, by kleing
list_all2_mono should not be [trans]
2003-12-23, by kleing
reorganised complex arithmetic
2003-12-23, by paulson
removing real_of_posnat
2003-12-23, by paulson
converting Hyperreal/NthRoot to Isar
2003-12-23, by paulson
converting Complex/Complex.ML to Isar
2003-12-23, by paulson
deleting redundant theorems
2003-12-23, by paulson
new theorems
2003-12-23, by paulson
tidying up hcomplex arithmetic
2003-12-23, by paulson
renaming some theorems
2003-12-23, by paulson
type hcomplex is now in class field
2003-12-23, by paulson
more ML bindings
2003-12-23, by paulson
added some [intro?] and [trans] for list_all2 lemmas
2003-12-23, by kleing
Updated proofs due to changes in Set.thy.
2003-12-22, by nipkow
converted Complex/NSComplex to Isar script
2003-12-22, by paulson
removal of the abel_cancel simproc for hypreal
2003-12-22, by paulson
downgrading abel_cancel
2003-12-22, by paulson
new binding
2003-12-22, by paulson
simplifying
2003-12-22, by paulson
moving HyperArith0.ML to other theories
2003-12-22, by paulson
removing obsolete bindings
2003-12-22, by paulson
tidying of HOL/Auth esp Guard lemmas
2003-12-21, by paulson
removed insert_Diff_single from simpset because it interfered with Auth :-(
2003-12-21, by nipkow
tidying first part of HyperArith0.ML, using generic lemmas
2003-12-19, by paulson
minor tweaks
2003-12-19, by paulson
type hypreal is an ordered field
2003-12-19, by paulson
*** empty log message ***
2003-12-19, by nipkow
tidied
2003-12-18, by paulson
*** empty log message ***
2003-12-18, by nipkow
converted Hyperreal/HyperDef to Isar script
2003-12-17, by paulson
fixed PG link
2003-12-16, by kleing
converted Hyperreal/HyperOrd to new-style theory
2003-12-16, by paulson
updated references to the now-pornographic proofgeneral.org
2003-12-15, by paulson
more general lemmas for Ring_and_Field
2003-12-15, by paulson
absolute value theorems moved to HOL/Ring_and_Field
2003-12-13, by paulson
moving some division theorems to Ring_and_Field
2003-12-12, by paulson
changed proof general links
2003-12-12, by kleing
Change to prune_prems in Pure/Isar/locale.ML.
2003-12-11, by ballarin
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
Added skalberg to recepients, changed admin from kleing to berghofe.
2003-08-27, by skalberg
Converted to new style theories.
2003-08-27, by skalberg
Prepared for extended identifiers (\<alpha>, etc.)
2003-08-27, by skalberg
Improved the error messages (slightly).
2003-08-27, by skalberg
Cleaned up the code.
2003-08-26, by skalberg
New specification syntax added (the specification may be split over
2003-08-26, by skalberg
Allowed for splitting the specification over several lemmas.
2003-08-26, by skalberg
Improved handling of modes for equality predicate, to avoid ill-typed
2003-08-22, by berghofe
Fixed problem with "code ind" attribute that caused code generator to
2003-08-21, by berghofe
Added function strong_conn for computing the strongly connected components
2003-08-21, by berghofe
Change from "tracing" to "warning", as requested by David Aspinall
2003-08-21, by paulson
final tweaks for Isar version
2003-08-20, by paulson
finished conversion to Isar format
2003-08-20, by paulson
new example
2003-08-20, by paulson
new case_tac method
2003-08-20, by paulson
partial conversion to Isar format
2003-08-20, by paulson
partial conversion to Isar format
2003-08-19, by paulson
new case_tac
2003-08-19, by paulson
For the Isar version of the ZF logics manual
2003-08-19, by paulson
converting ex/If to Isar script
2003-08-15, by paulson
A document for UNITY
2003-08-15, by paulson
reformatting change and mention of Introduction to Isabelle
2003-08-13, by paulson
corrections by Viktor Kuncak and minor updating
2003-08-13, by paulson
added tutorial
2003-08-13, by paulson
possibility proof!
2003-08-13, by paulson
ZhouGollmann: new example (fair non-repudiation protocol)
2003-08-12, by paulson
added lemma c_hupd_fst
2003-08-08, by streckem
Modifications after changes in MicroJava/J
2003-08-08, by streckem
Changed lemmas .._type_sound
2003-08-08, by streckem
Added lemma exec_no_xcpt
2003-08-08, by streckem
test_term now renames variable for size of test data to avoid clashes
2003-08-07, by berghofe
cleaned up
2003-08-05, by nipkow
*** empty log message ***
2003-07-31, by nipkow
Removed extraneous rev in function goal_params (the list of parameters
2003-07-31, by berghofe
opened new section for next Isabelle release
2003-07-29, by kleing
test_term now handles Match exception raised in generated code.
2003-07-28, by berghofe
Replaced \<leadsto> by \<rightharpoonup>
2003-07-25, by nipkow
Simplified a proof using presburger
2003-07-25, by paulson
new theory Library/NatPair
2003-07-24, by paulson
declarations moved from PreList.thy
2003-07-24, by paulson
Fixed two bugs:
2003-07-24, by berghofe
Exported function get_mode.
2003-07-24, by berghofe
header comment
2003-07-24, by paulson
new theory NatPair of the injection from nat*nat -> nat
2003-07-24, by paulson
Tidying and replacement of some axioms by specifications
2003-07-24, by paulson
tidied
2003-07-24, by paulson
Added some regression testing for simprocs
2003-07-22, by paulson
fixed simprocs
2003-07-22, by paulson
Added handling of meta implication and meta quantification.
2003-07-21, by skalberg
Added handling of free variables (provided they are of sort HOL.type).
2003-07-21, by skalberg
Tidied some examples
2003-07-21, by paulson
Added the specification command.
2003-07-21, by skalberg
Changed bstring argument to xstring.
2003-07-21, by skalberg
*** empty log message ***
2003-07-21, by skalberg
Added optional theorem names for the constant definitions added during
2003-07-19, by skalberg
Added package for definition by specification.
2003-07-17, by skalberg
tidying
2003-07-16, by paulson
Fixing a simproc bug
2003-07-15, by paulson
tidying
2003-07-15, by paulson
Some new thm (ex_map_conv?)
2003-07-15, by nipkow
use Library.Some/None instead of just Some/None in generated quickcheck code
2003-07-14, by kleing
Added keywords for random testing.
2003-07-11, by berghofe
Restored old (tail recursive!) version of repeat.
2003-07-11, by berghofe
Exported function goal_params.
2003-07-11, by berghofe
Added several functions for producing random numbers.
2003-07-11, by berghofe
Added functions for random testing.
2003-07-11, by berghofe
Added generator for test case generators.
2003-07-11, by berghofe
mk_int now produces specific constants for 0 and 1.
2003-07-11, by berghofe
- Installed specific code generator for equality enforcing that
2003-07-11, by berghofe
added upd_fst, upd_snd, some thms
2003-07-11, by oheimb
added map_image, restrict_map, some thms
2003-07-11, by oheimb
added fold_red, o2l, postfix, some thms
2003-07-11, by oheimb
added rev_ballE
2003-07-11, by oheimb
re-introduced sort constraints on LHS
2003-07-11, by oheimb
corrected markup text
2003-07-11, by oheimb
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
2003-07-10, by paulson