Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-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.
removed dead/duplicate code;
2009-09-29, by wenzelm
aliases for Thomas Sewell;
2009-09-29, by wenzelm
modernized Balanced_Tree;
2009-09-29, by wenzelm
replaced meta_iffD2 by existing Drule.equal_elim_rule2;
2009-09-29, by wenzelm
tuned header;
2009-09-29, by wenzelm
Thomas Sewell, NICTA: more efficient HOL/record implementation;
2009-09-29, by wenzelm
tuned whitespace -- recover basic Isabelle conventions;
2009-09-29, by wenzelm
merged
2009-09-29, by wenzelm
Merge with isabelle dev changes.
2009-09-29, by Thomas Sewell
Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
2009-09-29, by Thomas Sewell
Avoid a possible variable name conflict in instantiating a theorem.
2009-09-28, by Thomas Sewell
Fix unescaped expressions breaking latex output in Record.thy
2009-09-28, by Thomas Sewell
Merge record patch with updates from isabelle mainline.
2009-09-28, by Thomas Sewell
Avoid record-inner constants in polymorphic definitions in Bali
2009-09-25, by Thomas Sewell
Merge with changes from isabelle dev repository.
2009-09-24, by Thomas Sewell
Initial response to feedback from Norbert, Makarius on record patch
2009-09-23, by tsewell
Branch merge for isabelle mainline updates.
2009-09-22, by Thomas Sewell
Branch merge with updates from mainline isabelle.
2009-09-17, by Thomas Sewell
Implement previous fix (don't duplicate ext_def) correctly.
2009-09-11, by Thomas Sewell
There's no particular reason to duplicate the extension
2009-09-11, by Thomas Sewell
Merged with mainline changes.
2009-09-11, by Thomas Sewell
Adjust some documentation.
2009-09-11, by Thomas Sewell
Simplification of various aspects of the IsTuple component
2009-09-10, by Thomas Sewell
Record patch imported and working.
2009-09-10, by Thomas Sewell
Initial attempt at porting record update to repository Isabelle.
2009-08-27, by tsewell
Synchronized and Unsynchronized;
2009-09-29, by wenzelm
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
2009-09-29, by wenzelm
explicit indication of Unsynchronized.ref;
2009-09-29, by wenzelm
open_unsynchronized for interactive Isar loop;
2009-09-29, by wenzelm
explicit indication of Unsynchronized.ref;
2009-09-29, by wenzelm
Raw ML references as unsynchronized state variables.
2009-09-29, by wenzelm
Dummy version of state variables -- plain refs for sequential access.
2009-09-28, by wenzelm
reactivated at-sml-dev-e;
2009-09-28, by wenzelm
misc tuning and modernization;
2009-09-28, by wenzelm
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-28, by wenzelm
merged
2009-09-28, by wenzelm
less auxiliary functions
2009-09-28, by haftmann
tuned
2009-09-28, by haftmann
shared code between rep_datatype and datatype
2009-09-28, by haftmann
further unification of datatype and rep_datatype
2009-09-28, by haftmann
avoid compound fields in datatype info record
2009-09-28, by haftmann
fold_body_thms: pass pthm identifier;
2009-09-28, by wenzelm
tuned internal source structure;
2009-09-28, by wenzelm
added fork_deps_pri;
2009-09-28, by wenzelm
merged
2009-09-28, by haftmann
explicit pointless checkpoint
2009-09-28, by haftmann
emerging common infrastructure for datatype and rep_datatype
2009-09-27, by haftmann
streamlined rep_datatype further
2009-09-27, by haftmann
simplified rep_datatype
2009-09-27, by haftmann
more appropriate order of field in dt_info
2009-09-27, by haftmann
re-established reasonable inner outline for module
2009-09-27, by haftmann
merged
2009-09-27, by wenzelm
adjusted to changes in datatype package
2009-09-27, by haftmann
merged
2009-09-27, by haftmann
dropped dead code
2009-09-27, by haftmann
registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-09-27, by haftmann
fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
2009-09-27, by wenzelm
tuned;
2009-09-27, by wenzelm
reachable: recovered reverse post-order (lost in 73ad4884441f), which is expected for all_preds/all_succs and required for topological_order;
2009-09-27, by wenzelm
merged
2009-09-25, by paulson
New lemmas involving the real numbers, especially limits and series
2009-09-25, by paulson
NEWS; corrected spelling
2009-09-25, by haftmann
merged
2009-09-25, by haftmann
simplified proof
2009-09-23, by haftmann
removed potentially dangerous rules from pred_set_conv
2009-09-23, by haftmann
explicitly hide empty, inter, union
2009-09-23, by haftmann
merged
2009-09-23, by haftmann
merged
2009-09-23, by haftmann
merged
2009-09-23, by haftmann
inf/sup_absorb are no default simp rules any longer
2009-09-23, by haftmann
merged
2009-09-22, by haftmann
merged
2009-09-21, by haftmann
adapted proof
2009-09-21, by haftmann
merged
2009-09-21, by haftmann
tuned proofs
2009-09-21, by haftmann
tuned header
2009-09-21, by haftmann
added note on simp rules
2009-09-21, by haftmann
merged
2009-09-21, by haftmann
tuned proof; tuned headers
2009-09-21, by haftmann
merged
2009-09-21, by haftmann
tuned proofs; be more cautios wrt. default simp rules
2009-09-21, by haftmann
merged
2009-09-21, by haftmann
tuned proofs
2009-09-21, by haftmann
merged
2009-09-19, by haftmann
inter and union are mere abbreviations for inf and sup
2009-09-19, by haftmann
merged
2009-09-24, by haftmann
lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
2009-09-24, by haftmann
subsumed by more general setup in List.thy
2009-09-24, by haftmann
idempotency case for fold1
2009-09-24, by haftmann
added dual for complete lattice
2009-09-24, by haftmann
merged
2009-09-24, by nipkow
record how many "proof"s are solved by s/h
2009-09-24, by nipkow
added quotes for filenames;
2009-09-24, by boehmes
merged; adopted to changes from Code_Evaluation in the predicate compiler
2009-09-24, by bulwahn
replaced sorry by oops; removed old debug functions in predicate compiler
2009-09-23, by bulwahn
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
2009-09-23, by bulwahn
adapted configuration for DatatypeCase.make_case
2009-09-23, by bulwahn
added a new example for the predicate compiler
2009-09-23, by bulwahn
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
2009-09-23, by bulwahn
added first prototype of the extended predicate compiler
2009-09-23, by bulwahn
moved predicate compiler to Tools
2009-09-23, by bulwahn
removed generation of strange tuple modes in predicate compiler
2009-09-23, by bulwahn
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
2009-09-23, by bulwahn
modified predicate compiler further to support tuples
2009-09-23, by bulwahn
changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
2009-09-23, by bulwahn
handling of definitions
2009-09-23, by bulwahn
experimenting to add some useful interface for definitions
2009-09-23, by bulwahn
added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
2009-09-23, by bulwahn
modified handling of side conditions in proof procedure of predicate compiler
2009-09-23, by bulwahn
merged
2009-09-23, by haftmann
Code_Eval(uation)
2009-09-23, by haftmann
merged
2009-09-23, by blanchet
Added "nitpick_const_simp" tags to lazy list theories.
2009-09-23, by blanchet
atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
2009-09-23, by krauss
merged
2009-09-23, by haftmann
stripped legacy ML bindings
2009-09-23, by haftmann
Undo errornous commit of Statespace change
2009-09-23, by hoelzl
correct variable order in approximate-method
2009-09-23, by hoelzl
merged
2009-09-23, by paulson
Correct chasing of type variable instantiations during type unification.
2009-09-23, by paulson
hide newly introduced constants
2009-09-23, by haftmann
used standard fold function and type aliases
2009-09-22, by Philipp Meyer
sos method generates and uses proof certificates
2009-09-21, by Philipp Meyer
full reserve of worker threads -- for improved CPU utilization;
2009-09-22, by wenzelm
merged
2009-09-22, by haftmann
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-09-22, by haftmann
tail -n 20: more helpful output if make fails
2009-09-22, by krauss
corrected order of type variables in code equations; more precise certificate for cases
2009-09-22, by haftmann
merged
2009-09-21, by Christian Urban
tuned some proofs
2009-09-21, by Christian Urban
merged
2009-09-21, by haftmann
added session theory for Bali and Nominal_Examples
2009-09-21, by haftmann
added session theory for Nominal_Examples
2009-09-21, by haftmann
added session theory for Bali
2009-09-21, by haftmann
adjusted to new Number Theory scenario
2009-09-21, by haftmann
added session entry point theories
2009-09-21, by haftmann
common base for protocols with symmetric keys
2009-09-21, by haftmann
tuned header
2009-09-21, by haftmann
isarified proof
2009-09-21, by haftmann
fixed permissions -- this is a script, not an executable;
2009-09-21, by wenzelm
tuned;
2009-09-21, by wenzelm
deleted unused file
2009-09-21, by boehmes
merged
2009-09-21, by haftmann
entry point theory for examples; reactivated half-dead example
2009-09-21, by haftmann
merged
2009-09-21, by boehmes
corrected remote SMT solver invocation
2009-09-21, by boehmes
theory entry point for session Hoare_Parallel (now also with proper underscore)
2009-09-21, by haftmann
merged
2009-09-21, by boehmes
tuned author
2009-09-21, by boehmes
added new method "smt": an oracle-based connection to external SMT solvers
2009-09-18, by boehmes
tuned tracing;
2009-09-20, by wenzelm
scheduler backdoor: 9999 means 1 worker;
2009-09-20, by wenzelm
Hilbert_Classical: more precise control of parallel_proofs;
2009-09-20, by wenzelm
actually observe Multithreading.enabled (cf. d302f1c9e356);
2009-09-20, by wenzelm
merged
2009-09-19, by nipkow
restructured code
2009-09-19, by nipkow
merged
2009-09-19, by haftmann
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
2009-09-18, by haftmann
modified minimization log
2009-09-18, by nipkow
merged
2009-09-18, by nipkow
skip &&& goals
2009-09-18, by nipkow
INTER and UNION are mere abbreviations for INFI and SUPR
2009-09-18, by haftmann
simplified proof
2009-09-18, by haftmann
partially isarified proof
2009-09-18, by haftmann
tuned const_name antiquotations
2009-09-18, by haftmann
more antiquotations
2009-09-18, by haftmann
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
2009-09-18, by haftmann
tuned NEWS, added CONTRIBUTORS
2009-09-18, by haftmann
merged
2009-09-17, by nipkow
removed misleading log line
2009-09-17, by nipkow
NEWS: New method metisFT
2009-09-17, by paulson
New theorems for proving equalities and inclusions involving unions
2009-09-17, by paulson
added time limit for extraction phase (not supported on Cygwin)
2009-09-17, by boehmes
merged
2009-09-17, by boehmes
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
2009-09-17, by boehmes
Synchronized.value does not require locking, since assigments are atomic;
2009-09-16, by wenzelm
tuned;
2009-09-16, by wenzelm
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
2009-09-16, by wenzelm
merged
2009-09-16, by haftmann
Inter and Union are mere abbreviations for Inf and Sup; tuned
2009-09-16, by haftmann
Inter and Union are mere abbreviations for Inf and Sup
2009-09-16, by haftmann
merged
2009-09-16, by nipkow
revised lemma counting
2009-09-16, by nipkow
merged
2009-09-16, by haftmann
merged
2009-09-15, by haftmann
hide new constants
2009-09-15, by haftmann
merged
2009-09-15, by haftmann
restored code generation for OCaml
2009-09-15, by haftmann
added singleton example
2009-09-15, by haftmann
added emptiness check predicate and singleton projection
2009-09-15, by haftmann
added append_after (tuned version of former insert_after of Seq);
2009-09-16, by wenzelm
double linking for improved performance of "prev";
2009-09-15, by wenzelm
merged
2009-09-15, by wenzelm
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
2009-09-15, by boehmes
Isar.define_command: identify transaction;
2009-09-15, by wenzelm
updated bib;
2009-09-15, by wenzelm
count number of iterations required for minimization (and fixed bug: minimization was always called)
2009-09-14, by nipkow
merged
2009-09-14, by haftmann
more antiquotations
2009-09-14, by haftmann
some lemmas about strict order in lattices
2009-09-14, by haftmann
explicitly export type abbreviations (as usual in SML97);
2009-09-13, by wenzelm
wrapper for Real.fmt -- via StringCvt.realfmt;
2009-09-13, by wenzelm
made SML/NJ happy;
2009-09-13, by wenzelm
standard headers and text sections;
2009-09-12, by wenzelm
merged
2009-09-11, by nipkow
Made record parameter flexible to allow for extensions
2009-09-11, by nipkow
merged
2009-09-11, by haftmann
corrected upper/lowercase
2009-09-11, by haftmann
merged
2009-09-10, by haftmann
obey underscore naming convention
2009-09-10, by haftmann
plain structure name; signature constraint; shorter lines
2009-09-10, by haftmann
split of test examples from NatTransfer
2009-09-10, by haftmann
generic transfer procedure
2009-09-10, by haftmann
early bootstrap of generic transfer procedure
2009-09-10, by haftmann
cleanedup theorems all_nat ex_nat
2009-09-10, by haftmann
atp_minimize is now not using whitelist
2009-09-10, by Philipp Meyer
position information is now passed to all actions;
2009-09-10, by nipkow
logging number of metis lemmas
2009-09-10, by nipkow
minimization: comparing w/ and w/o.
2009-09-09, by nipkow
merged
2009-09-09, by haftmann
dropped accidental code additions
2009-09-09, by haftmann
merged
2009-09-09, by haftmann
explicit transfer avoids spurious merge problems
2009-09-09, by haftmann
moved eq handling in nbe into separate oracle
2009-09-09, by haftmann
tuned document -- proper text instead of source comments, reduced line length;
2009-09-08, by wenzelm
fixed cleanup routine in neos csdp script
2009-09-01, by Philipp Meyer
timeout option for ATPs
2009-09-08, by boehmes
merged
2009-09-07, by wenzelm
modernized Event_Bus -- based on actors;
2009-09-07, by wenzelm
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
2009-09-07, by nipkow
merged
2009-09-07, by nipkow
tuned stats
2009-09-07, by nipkow
Fixed a few problems with the method metisFT
2009-09-07, by paulson
merged
2009-09-07, by nipkow
tuned stats
2009-09-07, by nipkow
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
2009-09-07, by paulson
merged
2009-09-07, by paulson
conflict resolution possibly
2009-09-07, by paulson
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
2009-09-04, by paulson
merged
2009-08-28, by paulson
More streamlining using metis.
2009-08-27, by paulson
enabled metis permanently, tuned stats
2009-09-07, by nipkow
added signature ATP_MINIMAL,
2009-09-05, by boehmes
merged
2009-09-05, by boehmes
separate output of ATP user time and sledgehammer (ML code) user time
2009-09-05, by boehmes
Mirabelle: command-line action options may either be key=value or just key
2009-09-05, by boehmes
added initialization and cleanup of actions,
2009-09-05, by boehmes
merged
2009-09-04, by haftmann
tuned metis proofs
2009-09-04, by haftmann
tuned
2009-09-04, by boehmes
tuned output
2009-09-04, by nipkow
merged
2009-09-03, by boehmes
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
2009-09-03, by boehmes
merged
2009-09-03, by haftmann
merged
2009-09-03, by haftmann
proper class syntax for sublocale class < expr
2009-09-03, by haftmann
added option full_typed for sledgehammer action
2009-09-03, by boehmes
added runtime information to sledgehammer
2009-09-03, by boehmes
tuned
2009-09-03, by boehmes
scaled avg_time
2009-09-03, by nipkow
merged
2009-09-03, by nipkow
tuned
2009-09-03, by nipkow
isatest: collect test results and logs in testdata repository
2009-09-03, by krauss
replaced backlist by whitelist
2009-09-03, by boehmes
Mirabelle: logging of exceptions (works only for PolyML)
2009-09-03, by boehmes
merged
2009-09-02, by wenzelm
refined delay into delay_first/delay_last;
2009-09-02, by wenzelm
merged
2009-09-02, by boehmes
add report script for Mirabelle
2009-09-02, by boehmes
Mirabelle: actions are responsible for handling exceptions,
2009-09-02, by boehmes
removed errors overseen in previous changes
2009-09-02, by boehmes
moved Mirabelle from HOL/Tools to HOL,
2009-09-02, by boehmes
removed unused signature
2009-09-02, by boehmes
explicit checks;
2009-09-02, by wenzelm
updated Poly/ML SVN version;
2009-09-02, by wenzelm
eval/location_props: always produce YXML markup, independent of print_mode;
2009-09-02, by wenzelm
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-09-02, by wenzelm
tuned ML message;
2009-09-02, by wenzelm
added "using" to blacklist
2009-09-02, by nipkow
merged
2009-09-02, by wenzelm
merged
2009-09-02, by wenzelm
removed old Isar document model;
2009-09-01, by wenzelm
corrected spelling
2009-09-01, by haftmann
merged
2009-09-01, by haftmann
added -q switch for run in qnd mode
2009-09-01, by haftmann
code generator is now a separate component
2009-09-01, by haftmann
tuned document
2009-09-01, by haftmann
some reorganization of number theory
2009-09-01, by haftmann
some reorganization of number theory
2009-09-01, by haftmann
merged
2009-09-01, by haftmann
tuned
2009-09-01, by haftmann
avoid long line
2009-08-24, by haftmann
added txt to blacklist
2009-09-01, by nipkow
Isabelle_Process: receiver as Actor, not EventBus;
2009-09-01, by wenzelm
merged
2009-09-01, by boehmes
Mirabelle: actions are responsible for their log messages, output is better readable
2009-09-01, by boehmes
merged
2009-09-01, by wenzelm
merged
2009-09-01, by boehmes
Mirabelle: added preliminary documentation,
2009-09-01, by boehmes
Mirabelle: explicit command blacklist, preliminary documentation
2009-08-31, by boehmes
modernized Isar_Document;
2009-09-01, by wenzelm
modernized Thy_Header;
2009-09-01, by wenzelm
misc cleanup and internal reorganization;
2009-09-01, by wenzelm
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
2009-09-01, by wenzelm
moved lemma Wellfounded.in_inv_image to Relation.thy
2009-08-31, by krauss
moved wfrec to Recdef.thy
2009-08-31, by krauss
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
2009-08-31, by krauss
Mirabelle: handle possible parser exceptions, emit suitable log message
2009-08-31, by boehmes
merged
2009-08-31, by boehmes
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
2009-08-31, by boehmes
merged
2009-08-31, by nipkow
tuned the simp rules for Int involving insert and intervals.
2009-08-31, by nipkow
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
2009-08-31, by boehmes
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
2009-08-31, by boehmes
merged
2009-08-29, by boehmes
apply metis with found theorems in case sledgehammer was successful
2009-08-29, by boehmes
propagate theorem names, in addition to generated return message
2009-08-29, by boehmes
misc tuning;
2009-08-29, by wenzelm
eliminated hard tabs;
2009-08-29, by wenzelm
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
2009-08-29, by wenzelm
merged
2009-08-28, by wenzelm
fixed HOLogic.stringT
2009-08-28, by krauss
merged
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-08-28, by nipkow
New option ForceSystem that makes sure we *really* get the system we ask for
2009-08-28, by nipkow
selectable prover for sledgehammer, proper environment lookup
2009-08-28, by boehmes
discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28, by wenzelm
modernized messages -- eliminated ctyp/cterm operations;
2009-08-28, by wenzelm
removed spurious invocations of atp_minimize;
2009-08-28, by wenzelm
removed obsolete print_ctyp, print_cterm;
2009-08-28, by wenzelm
modernized messages -- eliminated old Display.print_cterm;
2009-08-28, by wenzelm
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
2009-08-28, by wenzelm
misc updates and tuning;
2009-08-28, by wenzelm
PDF_VIEWER: more Unix-ish behaviour on Mac OS;
2009-08-28, by wenzelm
merged
2009-08-27, by nipkow
New example: IMP
2009-08-27, by nipkow
merged
2009-08-27, by nipkow
code generator: quantifiers over {_.._::int} and {_..<_::nat}
2009-08-27, by nipkow
more stats;
2009-08-27, by wenzelm
tuned tracing;
2009-08-27, by wenzelm
merged
2009-08-27, by wenzelm
avoid macbroy21 for now -- hardware problems;
2009-08-27, by wenzelm
tuned code generation for lists
2009-08-27, by nipkow
merged
2009-08-26, by nipkow
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
2009-08-26, by nipkow
merged
2009-08-26, by chaieb
merged
2009-08-26, by chaieb
removed unused theorem finite_Atleast_Atmost
2009-08-26, by chaieb
merged
2009-05-19, by chaieb
Derivative of general reverses
2009-05-19, by chaieb
merged
2009-08-26, by nipkow
new interval lemma
2009-08-26, by nipkow
merged
2009-08-26, by paulson
Simplified some proofs using metis.
2009-08-26, by paulson
merged
2009-08-21, by paulson
sledgehammer used to streamline protocol proofs
2009-08-14, by paulson
Put back characters that had been erased by Emacs
2009-08-14, by paulson
added further conversions and conversionals
2009-08-26, by boehmes
merged
2009-08-26, by nipkow
new lemmas
2009-08-26, by nipkow
some examples for giving measures manually
2009-08-24, by krauss
stricter condition for (binary) integer relation
2009-08-24, by boehmes
more quoting for shell variables, canonical isabelle process
2009-08-24, by boehmes
keep the modified (tested) theory,
2009-08-24, by boehmes
do not introduce additional newlines
2009-08-24, by boehmes
tuned;
2009-08-22, by wenzelm
generalized settings;
2009-08-22, by wenzelm
removed jedit setup -- now a self-contained component (external);
2009-08-22, by wenzelm
less ambitious array operations -- for improved compatibility with older versions of bash;
2009-08-22, by wenzelm
function splitarray: splightly more abstract version that accomodates older bashes;
2009-08-22, by wenzelm
fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)
2009-08-21, by krauss
added Mirabelle to NEWS
2009-08-21, by boehmes
merged
2009-08-21, by boehmes
disabled refute action (needs changes in the code of refute)
2009-08-21, by boehmes
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
2009-08-21, by boehmes
moved Mirabelle to HOL/Tools
2009-08-21, by boehmes
moved Mirabelle to HOL/Tools
2009-08-21, by boehmes
Mirabelle tool script conforming to standard Isabelle tool interface,
2009-08-21, by boehmes
made Mirabelle a component
2009-08-17, by boehmes
A few Isar scripts
2009-08-20, by paulson
additional checkpoints avoid problems in error situations
2009-08-15, by haftmann
tuned
2009-08-15, by haftmann
removed atp_minimize invocation
2009-08-14, by krauss
reverted accidential corruption of superscripts introduced in a508148f7c25
2009-08-14, by krauss
merged
2009-08-14, by haftmann
inserted space into message
2009-08-14, by haftmann
formally stylized
2009-08-14, by haftmann
formally stylized
2009-08-14, by haftmann
corrected Pair to Char
2009-08-14, by haftmann
merged
2009-08-14, by webertj
Fixed a bug where the simplifier would hang on
2009-08-14, by webertj
merged
2009-08-13, by paulson
Removal of redundant settings of unification trace and search bounds.
2009-08-13, by paulson
Demonstrations of sledgehammer in protocol proofs.
2009-08-13, by paulson
added PARALLEL_CHOICE, PARALLEL_GOALS;
2009-08-12, by wenzelm
merged
2009-08-11, by wenzelm
SOS: function to set default prover; output channel changed
2009-08-10, by Philipp Meyer
interrupt handler for neos csdp client
2009-08-10, by Philipp Meyer
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
2009-08-11, by wenzelm
updated generated document
2009-08-11, by haftmann
dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML
2009-08-11, by haftmann
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
2009-08-11, by haftmann
merged
2009-08-11, by haftmann
temporary adjustment to dubious state of eta expansion in recfun_codegen
2009-08-11, by haftmann
properly merged
2009-08-10, by haftmann
same_typscheme replaces ugly common_typ_eqns
2009-08-10, by haftmann
moved all technical processing of code equations to code_thingol.ML
2009-08-10, by haftmann
added map_transpose
2009-08-10, by haftmann
merged
2009-08-10, by haftmann
attempt to move desymbolization to translation
2009-08-10, by haftmann
added a somehow clueless comment
2009-07-31, by haftmann
repair mess produced by resolution afterwards
2009-07-31, by haftmann
using certify_instantiate
2009-07-31, by haftmann
merged
2009-07-31, by haftmann
cleaned up variable desymbolification and argument expansion
2009-07-31, by haftmann
more appropriate printing of function terms
2009-07-30, by haftmann
improved handling of parameters
2009-07-30, by haftmann
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-07-30, by haftmann
towards proper handling of argument order in comprehensions
2009-07-30, by haftmann
cleaned up
2009-07-30, by haftmann
termT and term_of_const
2009-07-30, by haftmann
added bij lemmas
2009-08-10, by nipkow
new lemma bij_comp
2009-08-10, by nipkow
refined mac-poly64 tests;
2009-08-08, by wenzelm
tuned spacing of sections;
2009-08-07, by wenzelm
more platforms;
2009-08-06, by wenzelm
tuned header;
2009-08-06, by wenzelm
misc changes to SOS by Philipp Meyer:
2009-08-06, by wenzelm
settings for ATP_Manager component;
2009-08-05, by wenzelm
merged
2009-08-05, by wenzelm
SUBPROOF: recovered Goal.check_finished;
2009-08-05, by wenzelm
added Isabelle_System.components;
2009-08-04, by wenzelm
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
2009-08-04, by wenzelm
etc/components;
2009-08-04, by wenzelm
turned object-logics into components;
2009-08-04, by wenzelm
spelling;
2009-08-04, by wenzelm
tuned "Bootstrapping the environment";
2009-08-04, by wenzelm
change IFS only locally -- thanks to bash arrays;
2009-08-04, by wenzelm
more uniform handling of ISABELLE_HOME_USER component;
2009-08-04, by wenzelm
options for more precise performance figures of at-poly, which happens to run on macbroy21;
2009-08-04, by wenzelm
removing tracing messages in predicate compiler
2009-08-04, by bulwahn
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
2009-08-04, by bulwahn
commented rpred compilation; tuned
2009-08-04, by bulwahn
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
2009-08-04, by bulwahn
tuned proof procedure; added size-limiting predicate compilation of higher order predicates; added guessing of number parameters for registrating predicates; removed debug messages
2009-08-04, by bulwahn
changed resolving depending predicates and fetching in the predicate compiler
2009-08-04, by bulwahn
refactoring predicate compiler; repaired proof procedure to handle all test cases
2009-08-04, by bulwahn
refactoring predicate compiler; added type synonyms and functions split_smode and split_mode
2009-08-04, by bulwahn
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
2009-08-04, by bulwahn
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
2009-08-04, by bulwahn
imported patch changed mode inference of predicate compiler to return infered dataflow
2009-08-04, by bulwahn
imported patch generic compilation of predicate compiler with different monads
2009-08-04, by bulwahn
exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory
2009-08-04, by bulwahn
removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
2009-08-04, by bulwahn
basic support for components (which imitate the usual Isabelle directory layout);
2009-08-04, by wenzelm
Tuned.
2009-08-02, by berghofe
the derived induction principles can be given an explicit name
2009-08-02, by Christian Urban
updated Variable.import;
2009-08-01, by wenzelm
merged
2009-08-01, by wenzelm
merged
2009-08-01, by wenzelm
modernized generated example session;
2009-07-31, by wenzelm
added Mirabelle
2009-07-31, by boehmes
Quickcheck callable from ML
2009-07-31, by boehmes
future scheduler: uninterruptible cancelation;
2009-08-01, by wenzelm
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
2009-08-01, by wenzelm
recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;
2009-07-30, by wenzelm
tuned tracing;
2009-07-30, by wenzelm
ISABELLE_USEDIR_OPTIONS: -q 2 by default;
2009-07-30, by wenzelm
merged
2009-07-30, by wenzelm
merged
2009-07-30, by wenzelm
merged
2009-07-30, by haftmann
cleaned up abstract tuple operations and named them consistently
2009-07-29, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip