Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+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.
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13, by wenzelm
*** empty log message ***
2005-04-13, by wenzelm
new signalling primmitives for sml/nj compatibility
2005-04-13, by paulson
*** empty log message ***
2005-04-12, by nipkow
tweaks mainly to achieve sml/nj compatibility
2005-04-12, by paulson
fixing an incompatibility with Posix.IO.mkTextReader
2005-04-12, by paulson
auto update
2005-04-11, by paulson
removal of Main and other tidying up
2005-04-11, by paulson
First release of interpretation commands.
2005-04-11, by ballarin
tuned
2005-04-11, by nipkow
added \restriction
2005-04-11, by nipkow
tuned Map, renamed lex stuff in List.
2005-04-11, by nipkow
Added lots of AMS harpoons
2005-04-10, by nipkow
_(_|_) is now override_on
2005-04-10, by nipkow
tuned
2005-04-10, by nipkow
section on qmark
2005-04-10, by nipkow
fixed the syntax of infix declarations
2005-04-09, by paulson
thmref: selection syntax;
2005-04-09, by wenzelm
update syntax of 'where' and 'of';
2005-04-09, by wenzelm
added PDF_VIEWER, ISABELLE_DOC_FORMAT;
2005-04-09, by wenzelm
Reconstruction code, now packaged to avoid name clashes
2005-04-08, by paulson
temporarily removed ATP code
2005-04-08, by paulson
removed bad code
2005-04-07, by paulson
Changed prob1.dfg to prob_1.dfg
2005-04-07, by quigley
Got rid of Main.thy reference
2005-04-07, by quigley
Integrating the reconstruction files into the building of HOL
2005-04-07, by quigley
Reconstruction.thy and IsaMakefile updated
2005-04-07, by quigley
*** empty log message ***
2005-04-07, by nipkow
new meta-level rules
2005-04-07, by paulson
*** empty log message ***
2005-04-07, by nipkow
reverted renaming of Some/None in comments and strings;
2005-04-07, by wenzelm
added term_8;
2005-04-07, by wenzelm
added get_axiom_i, invoke_oracle_i;
2005-04-07, by wenzelm
Drule.add_used;
2005-04-07, by wenzelm
invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!
2005-04-07, by wenzelm
added add_used; include tpairs;
2005-04-07, by wenzelm
improved exn_message;
2005-04-07, by wenzelm
Thm.invoke_oracle_i;
2005-04-07, by wenzelm
Scan.peek;
2005-04-07, by wenzelm
tuned updates, added map_entry;
2005-04-07, by wenzelm
added some, peek, trace'; tuned;
2005-04-07, by wenzelm
added header;
2005-04-07, by wenzelm
improved comments;
2005-04-07, by wenzelm
reverted renaming of Some/None in comments and strings;
2005-04-07, by wenzelm
handle Option instead of OPTION;
2005-04-07, by wenzelm
updated it
2005-04-06, by nipkow
watcher.ML and watcher.sig changed. Debug files now write to tmp.
2005-04-06, by quigley
Current version of res_atp.ML - causes an error when I run it. C.Q.
2005-04-05, by quigley
lexicographic order by Norbert Voelker
2005-04-05, by paulson
arg_cong2 by Norbert Voelker
2005-04-05, by paulson
*** empty log message ***
2005-04-05, by nipkow
Updated to add watcher code.
2005-04-04, by quigley
CVSfj
2005-04-04, by quigley
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
2005-04-02, by huffman
converted to new-style theory
2005-04-02, by huffman
convert to new-style theory
2005-04-01, by huffman
x-symbols and other tidying
2005-04-01, by paulson
Updated import configuration.
2005-04-01, by skalberg
bring make to delete files on error
2005-04-01, by gagern
patch to get it working again
2005-04-01, by paulson
*** empty log message ***
2005-03-31, by quigley
*** empty log message ***
2005-03-31, by quigley
*** empty log message ***
2005-03-31, by quigley
added theorems eta_cfun and cont2cont_eta
2005-03-31, by huffman
chfin now a subclass of po, proved instance chfin < cpo
2005-03-31, by huffman
cleaned up some proofs
2005-03-31, by huffman
fixed bug in prj' function
2005-03-31, by huffman
changed comments to text blocks, cleaned up a few proofs
2005-03-31, by huffman
converted from DOS to UNIX format
2005-03-30, by paulson
converted HOL-Subst to tactic scripts
2005-03-29, by paulson
conversion of UNITY to Isar scripts
2005-03-28, by paulson
new display of theory stamps
2005-03-26, by paulson
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-26, by gagern
use Library/Multiset instead of own definition
2005-03-26, by kleing
fixed typo (multiset_append)
2005-03-26, by kleing
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
2005-03-25, by aspinall
tidied up
2005-03-25, by paulson
Revert previous change (but leave comments).
2005-03-25, by aspinall
Support new PGIP commands redostep, redoitem
2005-03-25, by aspinall
Support non-standard file: URL syntax, temporarily.
2005-03-25, by aspinall
Further work on interpretation commands. New command `interpret' for
2005-03-24, by ballarin
*** empty log message ***
2005-03-24, by ballarin
Transitivity reasoner ignores types amenable to linear arithmetic.
2005-03-24, by ballarin
COMMENT IN WRONG PLACE
2005-03-24, by paulson
replaced bool by a new datatype "bit" for binary numerals
2005-03-23, by paulson
temporary removal of Import
2005-03-23, by paulson
tidied
2005-03-23, by paulson
auto update
2005-03-22, by paulson
deleted a pointless comment
2005-03-22, by paulson
ensuring that "equal" is not a function
2005-03-22, by paulson
auto update
2005-03-18, by paulson
meson now checks that problems are first-order
2005-03-17, by paulson
added string_of_term
2005-03-17, by nipkow
Bugfix related to the interpretation of IDT constructors
2005-03-17, by webertj
more concise ASCII escaping
2005-03-15, by paulson
fixed syntax for Let <x,y> = a in e
2005-03-14, by huffman
bug fixes involving typechecking clauses
2005-03-14, by paulson
removed theorems about Sinl_Rep and Sinr_Rep
2005-03-12, by huffman
simplified some definitions, many proofs are much shorter
2005-03-11, by huffman
minor Library.option related modifications
2005-03-11, by webertj
code reformatted
2005-03-11, by webertj
code reformatted
2005-03-11, by webertj
fixed bug: domain package can now define three or more mutually recursive types simultaneously
2005-03-11, by huffman
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
2005-03-11, by huffman
fixed filename in header
2005-03-10, by huffman
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
2005-03-10, by huffman
Registrations of global locale interpretations: improved, better naming.
2005-03-10, by ballarin
Debugging code (error_depth) removed.
2005-03-10, by ballarin
First version of global registration command.
2005-03-09, by ballarin
fix integer overflow in numeral syntax for SML NJ.
2005-03-08, by obua
fixed variable name
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
removed Cprod3_lemma1 and Cprod3_lemma2
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
added subsection headings, cleaned up some proofs
2005-03-08, by huffman
reordered and arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
arranged for document generation, cleaned up some proofs
2005-03-08, by huffman
added subsections and text for document generation
2005-03-07, by huffman
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
2005-03-07, by huffman
HTML 4.01 Transitional conformity
2005-03-07, by webertj
refute_params: default value itself=1 added (for type classes)
2005-03-07, by webertj
HTML 4.01 Transitional conformity
2005-03-07, by webertj
HTML 4.01 Transitional conformity
2005-03-07, by webertj
now checks for higher-order vars
2005-03-07, by paulson
Cleaning up HOL/Matrix
2005-03-07, by obua
Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-07, by paulson
add header
2005-03-04, by huffman
fix headers
2005-03-04, by huffman
converted to new-style theories, and combined numbered files
2005-03-04, by huffman
document generation for HOLCF
2005-03-04, by huffman
Removed practically all references to Library.foldr.
2005-03-04, by skalberg
new first_order test
2005-03-04, by paulson
removed dead code
2005-03-04, by paulson
interpreter for Finite_Set.Finites added
2005-03-03, by webertj
Move towards standard functions.
2005-03-03, by skalberg
fixed proof
2005-03-03, by nipkow
converted to new-style theory
2005-03-03, by huffman
converted to new-style theory
2005-03-03, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
another reorganization of setsums and intervals
2005-03-02, by nipkow
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
2005-03-02, by dixon
obscured the e-mail address lcp@cl
2005-03-02, by paulson
new lemmas int_diff_cases
2005-03-02, by paulson
eliminated deps for removed files
2005-03-02, by huffman
merged into Discrete.thy
2005-03-02, by huffman
converted to new-style theory
2005-03-02, by huffman
integrated Jeremy's FiniteLib
2005-03-01, by nipkow
spider dogding
2005-03-01, by kleing
added setsum_diff1' which holds in more general cases than setsum_diff1
2005-02-28, by obua
unfold theorems for trancl and rtrancl
2005-02-28, by paulson
lucas - added more comments and an extra type to clarify the code.
2005-02-27, by dixon
Modified node_trans to avoid duplication of signature stamps
2005-02-23, by berghofe
exception SAME removed
2005-02-23, by webertj
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
2005-02-23, by webertj
suminf -> \<Sum>
2005-02-23, by nipkow
Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
2005-02-22, by dixon
removed redundant lemmas and simprules
2005-02-22, by paulson
more setsum tuning
2005-02-22, by nipkow
more fine tuniung
2005-02-21, by nipkow
fixed proof
2005-02-21, by nipkow
removed superfluous setsum_constant
2005-02-21, by nipkow
comprehensive cleanup, replacing sumr by setsum
2005-02-21, by nipkow
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
2005-02-19, by dixon
continued eliminating sumr
2005-02-18, by nipkow
starting to get rid of sumr
2005-02-18, by nipkow
tuning
2005-02-18, by nipkow
*** empty log message ***
2005-02-16, by nipkow
refine now provides specific cases "goal1" ... "goaln" for addressing
2005-02-15, by berghofe
simplified a proof
2005-02-14, by paulson
Deleted Library.option type.
2005-02-13, by skalberg
Fully qualified refl and trans to avoid confusion with theorems
2005-02-11, by berghofe
Optimized present_tokens to produce fewer newlines when hiding proofs.
2005-02-11, by berghofe
New reference Toplevel.debug for verbose printing of exns.
2005-02-11, by ballarin
update from Larry
2005-02-11, by kleing
some stuff is now redundant.
2005-02-10, by nipkow
HOL.order -> Orderings.order due to restructering
2005-02-10, by nipkow
Moved oderings from HOL into the new Orderings.thy
2005-02-10, by nipkow
Added paper by M. Takahashi.
2005-02-10, by berghofe
Added proof of eta-postponement theorem (using parallel eta-reduction).
2005-02-10, by berghofe
non-inductive fold1Set proofs
2005-02-10, by paulson
simplified a key lemma for foldSet
2005-02-10, by paulson
Toplevel.debug for debugging in Isar.
2005-02-10, by ballarin
Fixed bug in select_thm.
2005-02-10, by berghofe
Subscripts for theorem lists now start at 1.
2005-02-10, by berghofe
mention authors are acknowledged for isabelle-lemmas
2005-02-10, by kleing
more preview
2005-02-10, by kleing
pointer to isabelle-lemmas submission list
2005-02-10, by kleing
added lattice_locales
2005-02-09, by nipkow
Extracted generic lattice stuff to new Lattice_Locales.thy
2005-02-09, by nipkow
New
2005-02-09, by nipkow
new foldSet proofs
2005-02-09, by paulson
revised fold1 proofs
2005-02-09, by paulson
revised fold1 proofs
2005-02-09, by paulson
cvs merge problem fixed
2005-02-08, by nipkow
new treatment of fold1
2005-02-08, by paulson
Fixed lattice defns
2005-02-08, by nipkow
*** empty log message ***
2005-02-07, by nipkow
fixed latex problems by including bigsqcap
2005-02-07, by nipkow
fixed latex problems
2005-02-07, by nipkow
fixed mac line
2005-02-06, by paulson
Added Lattice locale
2005-02-05, by nipkow
clausification and proof reconstruction
2005-02-04, by paulson
comment
2005-02-04, by paulson
Added semi-lattice locales and reorganized fold1 lemmas
2005-02-04, by nipkow
added find_rewrites
2005-02-03, by nipkow
new treatment of demodulation in proof reconstruction
2005-02-03, by paulson
don't generate latex for LaTeXsugar and OptionalSugar
2005-02-03, by kleing
removed sugar.sty (obsolete for devel version)
2005-02-03, by kleing
not needed any more by LaTeXSugar
2005-02-03, by kleing
Document now applies to devel version (and Isabelle 2005)
2005-02-03, by kleing
Replaced application of subst by simplesubst in proof of app_Var_NF
2005-02-02, by berghofe
Replaced application of subst by simplesubst in proof of rev_induct
2005-02-02, by berghofe
tidying of some subst/simplesubst proofs
2005-02-02, by paulson
generalization and tidying
2005-02-02, by paulson
improved handling of chained facts
2005-02-02, by paulson
Max_le -> Max_ge
2005-02-02, by nipkow
fold and fol1 changes
2005-02-02, by nipkow
added [simp]
2005-02-02, by nipkow
link to PG FAQ for start up problem
2005-02-02, by kleing
the new subst tactic, by Lucas Dixon
2005-02-01, by paulson
renamed a few vars, added a lemma
2005-01-30, by nipkow
proof simpification
2005-01-28, by nipkow
moved sugar.sty to textinputs
2005-01-28, by kleing
-H false for showing proofs (not -H true)
2005-01-28, by kleing
fixed bugs
2005-01-27, by nipkow
- Proofs are now hidden by default when generating documents
2005-01-27, by berghofe
Proofs are now hidden by default.
2005-01-27, by berghofe
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip