Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+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.
conceal consts via name space, not tags;
2009-10-25, by wenzelm
allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-25, by wenzelm
switch to polyml-5.2.1 to see if it impacts performance;
2009-10-25, by wenzelm
merged
2009-10-25, by chaieb
Multivariate polynomials library over fields
2009-10-25, by chaieb
A theory of polynomials based on lists
2009-10-25, by chaieb
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
2009-10-25, by chaieb
merged
2009-10-25, by wenzelm
further changes due to the previous merge in the predicate compiler
2009-10-24, by bulwahn
merge -- imported from bulwahn d759e2728188;
2009-10-24, by wenzelm
removed tuple functions from the predicate compiler
2009-10-24, by bulwahn
improving the compilation with higher-order arguments in the predicate compiler
2009-10-24, by bulwahn
now the predicate compilere handles the predicate without introduction rules better as before
2009-10-24, by bulwahn
removed dead code; added examples
2009-10-24, by bulwahn
removed obsolete GeneratorPrem; clean-up after modularization; tuned
2009-10-24, by bulwahn
modularized the compilation in the predicate compiler
2009-10-24, by bulwahn
adapted parser for options in the predicate compiler
2009-10-24, by bulwahn
modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples
2009-10-24, by bulwahn
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
2009-10-24, by bulwahn
added skip_proof option; playing with compilation of depth-limited predicates
2009-10-24, by bulwahn
reinvestigating the compilation of the random computation in the predicate compiler
2009-10-24, by bulwahn
added option to generate random values to values command in the predicate compiler
2009-10-24, by bulwahn
commented out the random generator compilation in the example file
2009-10-24, by bulwahn
added option to execute depth-limited computations for the values command in the predicate compiler
2009-10-24, by bulwahn
renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
2009-10-24, by bulwahn
simplified and improved compilation of depth-limited search in the predicate compiler
2009-10-24, by bulwahn
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
2009-10-24, by bulwahn
removed unnecessary argument rpred in code_pred function
2009-10-24, by bulwahn
added option show_mode_inference; added splitting of conjunctions in expand_tuples
2009-10-24, by bulwahn
changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
2009-10-24, by bulwahn
further cleaning up
2009-10-24, by bulwahn
added option show_proof_trace
2009-10-24, by bulwahn
importing of polymorphic introduction rules with different schematic variable names
2009-10-24, by bulwahn
added option show_intermediate_results
2009-10-24, by bulwahn
continued cleaning up; moved tuple expanding to core
2009-10-24, by bulwahn
cleaned up debugging messages; added options to code_pred command
2009-10-24, by bulwahn
added first support for higher-order function translation
2009-10-24, by bulwahn
added to process higher-order arguments by adding new constants
2009-10-24, by bulwahn
cleaned up
2009-10-24, by bulwahn
added theory with alternative definitions for the predicate compiler; cleaned up examples
2009-10-24, by bulwahn
importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first
2009-10-24, by bulwahn
higher-order arguments in different rules are fixed to one name in the predicate compiler
2009-10-24, by bulwahn
changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
2009-10-24, by bulwahn
changed proof method to handle widen predicate in JinjaThreads
2009-10-24, by bulwahn
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
2009-10-24, by bulwahn
processing of tuples in introduction rules
2009-10-24, by bulwahn
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
2009-10-24, by bulwahn
developing an executable the operator
2009-10-24, by bulwahn
generalizing singleton with a default value
2009-10-24, by bulwahn
changed elimination preprocessing due to an error with a JinjaThread predicate
2009-10-24, by bulwahn
added test for higher-order function inductification; added debug messages
2009-10-24, by bulwahn
added filtering of case constants in the definition retrieval of the predicate compiler
2009-10-24, by bulwahn
extended core of predicate compiler to expand tuples in introduction rules
2009-10-24, by bulwahn
added tupled versions of examples for the predicate compiler
2009-10-24, by bulwahn
moved meta_fun_cong lemma into ML-file; tuned
2009-10-24, by bulwahn
merged
2009-10-25, by wenzelm
adapted Function_Lib (cf. b8cdd3d73022);
2009-10-25, by wenzelm
configuration flag "partials"
2009-10-24, by krauss
renamed auto_term.ML -> relation.ML
2009-10-23, by krauss
function package: more standard names for structures and files
2009-10-23, by krauss
renamed FundefDatatype -> Function_Fun
2009-10-23, by krauss
maintain position of formal entities via name space;
2009-10-24, by wenzelm
maintain explicit name space kind;
2009-10-24, by wenzelm
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24, by wenzelm
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-24, by wenzelm
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-24, by wenzelm
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-24, by wenzelm
maintain abstract entry, with position, identity etc.;
2009-10-24, by wenzelm
tuned message;
2009-10-24, by wenzelm
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
2009-10-24, by wenzelm
markup for formal entities, with "def" or "ref" occurrences;
2009-10-24, by wenzelm
handle Sorts.CLASS_ERROR instead of arbitrary exceptions;
2009-10-24, by wenzelm
reactivated isatest on macbroy6 -- 3h later to avoid overlap with backup daemon;
2009-10-23, by wenzelm
merged
2009-10-23, by haftmann
turned off old quickcheck
2009-10-23, by haftmann
pat_completeness gets its own file
2009-10-23, by krauss
ignore error messages produced by ATPs
2009-10-23, by boehmes
merged
2009-10-23, by haftmann
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)
2009-10-23, by haftmann
restored accidentally deleted submultiset
2009-10-22, by haftmann
multiset operations with canonical argument order
2009-10-22, by haftmann
arg_types_of auxiliary function; using multiset operations
2009-10-22, by haftmann
merged
2009-10-23, by haftmann
close thm derivations explicitly
2009-10-22, by haftmann
Fix a duplicate abbreviation || in etc/symbols.
2009-10-23, by tbourke
made SML/NJ happy;
2009-10-22, by wenzelm
updated session name;
2009-10-22, by wenzelm
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
2009-10-22, by wenzelm
merged
2009-10-22, by wenzelm
merged
2009-10-22, by wenzelm
merged
2009-10-21, by wenzelm
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
2009-10-21, by wenzelm
merged
2009-10-22, by wenzelm
explicit close_derivation
2009-10-22, by haftmann
merged
2009-10-22, by haftmann
map_range (and map_index) combinator
2009-10-22, by haftmann
dropped Datatype.distinct_simproc
2009-10-22, by haftmann
use Synchronized.assign to achieve actual immutable results;
2009-10-22, by wenzelm
support single-assigment variables -- based on magic RTS operations by David Matthews;
2009-10-22, by wenzelm
merged
2009-10-22, by boehmes
fixed permissions -- this is a script, not an executable
2009-10-22, by boehmes
inv_onto -> inv_into
2009-10-22, by nipkow
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-21, by blanchet
merged
2009-10-21, by blanchet
fixed the "expect" mechanism of Refute in the face of timeouts
2009-10-21, by blanchet
removed "nitpick_const_simp" attribute from Record's "simps";
2009-10-21, by blanchet
merged
2009-10-21, by haftmann
more accurate removal
2009-10-21, by haftmann
merged
2009-10-21, by haftmann
curried inter as canonical list operation (beware of argument order)
2009-10-21, by haftmann
merged
2009-10-21, by boehmes
proper handling of single literal case,
2009-10-21, by boehmes
Removed the hard-wired white list of theorems for sledgehammer
2009-10-21, by paulson
merged
2009-10-21, by paulson
Some new lemmas concerning sets
2009-10-20, by paulson
merged
2009-10-21, by haftmann
curried union as canonical list operation
2009-10-21, by haftmann
tuned ML import
2009-10-21, by haftmann
removed old-style \ and \\ infixes
2009-10-21, by haftmann
merged
2009-10-21, by haftmann
dropped redundant gen_ prefix
2009-10-21, by haftmann
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20, by haftmann
find_theorems: better handling of abbreviations (by Timothy Bourke)
2009-10-21, by kleing
standardized basic operations on type option;
2009-10-21, by wenzelm
eliminated THENL -- use THEN RANGE;
2009-10-20, by wenzelm
tuned;
2009-10-20, by wenzelm
fixed SML/NJ toplevel pp;
2009-10-20, by wenzelm
backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-20, by wenzelm
tuned;
2009-10-20, by wenzelm
uniform use of Integer.min/max;
2009-10-20, by wenzelm
modernized session SET_Protocol;
2009-10-20, by wenzelm
modernized session Metis_Examples;
2009-10-20, by wenzelm
modernized session Isar_Examples;
2009-10-20, by wenzelm
tuned header;
2009-10-20, by wenzelm
more accurate dependencies for HOL-SMT, which is a session with image;
2009-10-20, by wenzelm
removed unused map_force;
2009-10-20, by wenzelm
Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-20, by paulson
additional schematic rules for Z3's rewrite rule
2009-10-20, by boehmes
merged
2009-10-20, by nipkow
added Hilbert_Choice section
2009-10-20, by nipkow
merged
2009-10-20, by boehmes
eliminated extraneous wrapping of public records,
2009-10-20, by boehmes
proper exceptions instead of unhandled partiality
2009-10-20, by boehmes
footnote: inv via inv_onto
2009-10-20, by nipkow
added inv_def for compatibility as a lemma
2009-10-20, by nipkow
slightly less context-sensitive settings;
2009-10-20, by wenzelm
merged
2009-10-20, by wenzelm
corrected paths to certificates,
2009-10-20, by boehmes
added proof reconstructon for Z3,
2009-10-20, by boehmes
merged
2009-10-20, by wenzelm
merged
2009-10-20, by haftmann
more accurate checkpoints
2009-10-20, by haftmann
dropped lazy code equations
2009-10-19, by haftmann
CONTRIBUTORS
2009-10-19, by haftmann
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-19, by wenzelm
eliminated duplicate fold1 -- beware of argument order!
2009-10-19, by wenzelm
uniform use of Integer.add/mult/sum/prod;
2009-10-19, by wenzelm
Removed dead code in function mk_deftab.
2009-10-19, by berghofe
Removed unneeded reference to inv_def.
2009-10-19, by berghofe
Replaced inv by the_inv_onto.
2009-10-19, by berghofe
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
2009-10-19, by berghofe
fixed proof (cf. d1d4d7a08a66);
2009-10-18, by wenzelm
removed disjunctive group cancellation -- provers run independently;
2009-10-18, by wenzelm
tuned;
2009-10-18, by wenzelm
removed some unreferenced material;
2009-10-18, by wenzelm
merged
2009-10-18, by nipkow
certificates for sos
2009-10-18, by nipkow
merged
2009-10-18, by nipkow
added sums of squares for standard deviation
2009-10-18, by nipkow
merged
2009-10-18, by nipkow
Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-18, by nipkow
disable indent-tabs-mode in Proof General / Emacs;
2009-10-18, by wenzelm
merged
2009-10-17, by wenzelm
made SML/NJ happy;
2009-10-17, by wenzelm
Merged.
2009-10-17, by ballarin
Finished revisions of locales tutorial.
2009-10-17, by ballarin
Changed part of the examples to int.
2009-10-15, by ballarin
Save current state of locales tutorial.
2009-10-15, by ballarin
Observe order of declaration when printing registrations.
2009-10-15, by ballarin
disable sunbroy2 for now;
2009-10-17, by wenzelm
tuned/moved divide_and_conquer';
2009-10-17, by wenzelm
tuned;
2009-10-17, by wenzelm
removed separate record_quick_and_dirty_sensitive;
2009-10-17, by wenzelm
simplified tactics;
2009-10-17, by wenzelm
eliminated old List.foldr and OldTerm operations;
2009-10-17, by wenzelm
removed unused names;
2009-10-17, by wenzelm
misc tuning and simplification;
2009-10-17, by wenzelm
less pervasive names;
2009-10-17, by wenzelm
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17, by wenzelm
Method.cheating: check quick_and_dirty here;
2009-10-17, by wenzelm
tuned;
2009-10-17, by wenzelm
Unsynchronized.set etc.;
2009-10-17, by wenzelm
indicate CRITICAL nature of various setmp combinators;
2009-10-17, by wenzelm
ISABELLE_TOOL;
2009-10-17, by wenzelm
tuned signature;
2009-10-17, by wenzelm
merged
2009-10-17, by wenzelm
merged
2009-10-17, by nipkow
added the_inv_onto
2009-10-17, by nipkow
eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-17, by wenzelm
removed obsolete old goal command;
2009-10-17, by wenzelm
legacy Drule.standard is no longer pervasive;
2009-10-17, by wenzelm
explicitly qualify Drule.standard;
2009-10-17, by wenzelm
tuned white space;
2009-10-16, by wenzelm
local channels for tracing/debugging;
2009-10-16, by wenzelm
made SML/NJ happy;
2009-10-16, by wenzelm
sunbroy2: back to single-threaded mode for now -- deadlock in Poly/ML 5.3-SVN-900;
2009-10-15, by wenzelm
replaced String.concat by implode;
2009-10-15, by wenzelm
space_implode;
2009-10-15, by wenzelm
normalized aliases of Output operations;
2009-10-15, by wenzelm
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
2009-10-15, by wenzelm
natural argument order for prover;
2009-10-15, by wenzelm
ATP_Manager.get_prover: canonical argument order;
2009-10-15, by wenzelm
tuned proof (via atp_minimized);
2009-10-15, by wenzelm
sort_strings (cf. Pure/library.ML);
2009-10-15, by wenzelm
clarified File.platform_path vs. File.shell_path;
2009-10-15, by wenzelm
exported File.shell_quote;
2009-10-15, by wenzelm
misc tuning and recovery of Isabelle coding style;
2009-10-15, by wenzelm
eliminated extraneous wrapping of public records;
2009-10-15, by wenzelm
tuned signature;
2009-10-15, by wenzelm
renamed functor HeapFun to Heap;
2009-10-15, by wenzelm
misc tuning and clarification;
2009-10-15, by wenzelm
structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
2009-10-15, by wenzelm
modernized structure names;
2009-10-14, by wenzelm
show direct GC time (which is included in CPU time);
2009-10-14, by wenzelm
eliminated obsolete C/flip combinator;
2009-10-14, by wenzelm
added List.nth
2009-10-14, by nipkow
tuned make parameters for sunbroy2;
2009-10-14, by wenzelm
accomodate old version of "tail", e.g. on sunbroy2;
2009-10-14, by wenzelm
settings for parallel experimental Poly/ML 5.3;
2009-10-14, by wenzelm
sharpened name
2009-10-14, by haftmann
more explicit notion of canonized code equations
2009-10-14, by haftmann
more explicit notion of canonized code equations
2009-10-14, by haftmann
tuned whitespace
2009-10-14, by haftmann
tuned whitespace
2009-10-14, by haftmann
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
2009-10-14, by haftmann
merged
2009-10-13, by haftmann
deactivated Datatype.distinct_simproc
2009-10-13, by haftmann
dropped Datatype.distinct_simproc; tuned
2009-10-13, by haftmann
order conjunctions to be printed without parentheses
2009-10-13, by hoelzl
approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
2009-10-13, by hoelzl
merged
2009-10-13, by haftmann
added add_tyconames; tuned
2009-10-12, by haftmann
merged
2009-10-13, by haftmann
more appropriate abstraction over distinctness rules
2009-10-13, by haftmann
merged
2009-10-12, by haftmann
intro_base_names combinator
2009-10-12, by haftmann
merged
2009-10-12, by haftmann
dropped dist_ss
2009-10-12, by haftmann
merged
2009-10-12, by haftmann
added is_IVar
2009-10-12, by haftmann
factored out Code_Printer.aux_params
2009-10-12, by haftmann
dropped rule duplicates
2009-10-12, by haftmann
less non-standard combinators
2009-10-12, by haftmann
nth replaces List.nth
2009-10-12, by haftmann
dropped redundancy
2009-10-12, by haftmann
dropped dead code
2009-10-12, by haftmann
using distinct rules directly
2009-10-12, by haftmann
simplified proof
2009-10-09, by haftmann
dropped simproc_dist formally
2009-10-09, by haftmann
tuned order of lemmas
2009-10-09, by haftmann
term styles also cover antiquotations term_type and typeof
2009-10-09, by haftmann
merged
2009-10-09, by haftmann
lookup for datatype constructors considers type annotations to resolve overloading
2009-10-08, by haftmann
added group_stmts
2009-10-08, by haftmann
moved labelled_name to code_thingol
2009-10-08, by haftmann
updated generated documentation
2009-10-08, by haftmann
corrected syntax diagrams for styles
2009-10-08, by haftmann
new generalized concept for term styles
2009-10-08, by haftmann
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
2009-10-07, by haftmann
isatest: store test identifiers
2009-10-08, by krauss
tuned proofs
2009-10-07, by haftmann
added bot_boolE, top_boolI
2009-10-07, by haftmann
do not use Locale.add_registration_eqs any longer
2009-10-07, by haftmann
Inf/Sup now purely syntactic
2009-10-07, by haftmann
merged
2009-10-06, by haftmann
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-10-06, by haftmann
merged
2009-10-06, by haftmann
added Coset as constructor
2009-10-06, by haftmann
sets and cosets
2009-10-06, by haftmann
added syntactic Inf and Sup
2009-10-06, by haftmann
merged
2009-10-05, by paulson
New lemmas connected with the reals and infinite series
2009-10-05, by paulson
New facts about domain and range in
2009-10-05, by paulson
merged
2009-10-05, by haftmann
experimental de-facto abolishment of distinctness limit
2009-10-05, by haftmann
tuned handling of type variable names further
2009-10-05, by haftmann
variables in type schemes must be renamed simultaneously with variables in equations
2009-10-05, by haftmann
explicitly unsynchronized
2009-10-05, by haftmann
explicitly unsynchronized
2009-10-05, by haftmann
recovered support for Spass: re-enabled writing problems in DFG format
2009-10-04, by boehmes
avoid exception Option: only apply "the" if needed
2009-10-04, by boehmes
merged
2009-10-04, by nipkow
atp_minimal using chain_ths again
2009-09-30, by Philipp Meyer
merged
2009-10-03, by boehmes
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
2009-10-03, by boehmes
eliminated dead code;
2009-10-02, by wenzelm
eliminated dead code and redundant parameters;
2009-10-02, by wenzelm
eliminated dead code;
2009-10-02, by wenzelm
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02, by wenzelm
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02, by wenzelm
Refute.refute_goal: goal addressing from 1 as usual;
2009-10-02, by wenzelm
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
2009-10-02, by wenzelm
clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-10-02, by wenzelm
misc tuning and simplification;
2009-10-02, by wenzelm
macbroy2: bigger jobs first, to avoid danger of swapping during daytime;
2009-10-02, by wenzelm
less ambitious heap settings;
2009-10-02, by wenzelm
merged
2009-10-02, by haftmann
merged
2009-10-01, by haftmann
proper merge of interpretation equations
2009-10-01, by haftmann
merged
2009-10-02, by wenzelm
Merged again.
2009-10-01, by ballarin
Merged.
2009-10-01, by ballarin
News entry: inheritance of mixins; print_interps.
2009-10-01, by ballarin
Avoid administrative overhead for identity mixins.
2009-10-01, by ballarin
tuned;
2009-10-01, by wenzelm
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
2009-10-01, by wenzelm
added Ctermtab, cterm_cache, thm_cache;
2009-10-01, by wenzelm
added term_cache;
2009-10-01, by wenzelm
Concurrently cached values.
2009-10-01, by wenzelm
tuned header;
2009-10-01, by wenzelm
core_sos_tac: SUBPROOF body operates on subgoal 1;
2009-10-01, by wenzelm
merged
2009-10-01, by wenzelm
updated generated files;
2009-10-01, by wenzelm
enable slow-motion mode to accomodate unsynchronized refs within theory sources;
2009-10-01, by wenzelm
avoid unsynchronized refs within theory sources;
2009-10-01, by wenzelm
explicitly Unsynchronized;
2009-10-01, by wenzelm
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
2009-10-01, by Philipp Meyer
changed core_sos_tac to use SUBPROOF
2009-10-01, by Philipp Meyer
replaced and tuned uses of foldr1
2009-09-30, by Philipp Meyer
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
2009-09-30, by Philipp Meyer
removed opening of structures
2009-09-22, by Philipp Meyer
merged
2009-10-01, by wenzelm
merged
2009-10-01, by nipkow
merged
2009-10-01, by nipkow
made spass additional default prover
2009-10-01, by nipkow
merged
2009-10-01, by paulson
Proved a new theorem: nat_to_nat2_inj
2009-10-01, by paulson
turned unsynchronized ref into synchronized var
2009-10-01, by boehmes
merged
2009-10-01, by nipkow
resolved conflict
2009-10-01, by nipkow
record max lemmas used
2009-10-01, by nipkow
Lazy evaluation with memoing (sequential version).
2009-10-01, by wenzelm
more official status of sequential implementations;
2009-10-01, by wenzelm
separate concurrent/sequential versions of lazy evaluation;
2009-10-01, by wenzelm
added Task_Queue.depend (again) -- light-weight version for transitive graph;
2009-10-01, by wenzelm
handle Pattern.MATCH, not arbitrary exceptions;
2009-10-01, by wenzelm
more precise dependencies;
2009-10-01, by wenzelm
eliminated redundant parameters;
2009-10-01, by wenzelm
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
2009-10-01, by wenzelm
avoid mixed l/r infixes, which do not work in some versions of SML;
2009-10-01, by wenzelm
tuned;
2009-10-01, by wenzelm
merged
2009-10-01, by wenzelm
explicitly Unsynchronized
2009-10-01, by haftmann
Merged.
2009-10-01, by ballarin
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-29, by ballarin
Archive registrations by external view.
2009-09-27, by ballarin
Stricter test: raise error if registration generates duplicate theorem.
2009-09-26, by ballarin
Explicit management of registration mixins.
2009-09-19, by ballarin
Improved comments and api names.
2009-08-19, by ballarin
eliminated dead code, redundant bindings and parameters;
2009-10-01, by wenzelm
misc tuning and simplification;
2009-10-01, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
Sorts.of_sort_derivation: no pp here;
2009-09-30, by wenzelm
eliminated redundant bindings;
2009-09-30, by wenzelm
actually perform Isar_Document.init on startup;
2009-09-30, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
removed dead code;
2009-09-30, by wenzelm
handle Type.TYPE_MATCH, not arbitrary exceptions;
2009-09-30, by wenzelm
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
2009-09-30, by wenzelm
PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
2009-09-30, by wenzelm
actually export unit parser;
2009-09-30, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
eliminated redundant parameters;
2009-09-30, by wenzelm
eliminated redundant bindings;
2009-09-30, by wenzelm
merged
2009-09-30, by haftmann
moved lemmas about sup on bool to Lattices.thy
2009-09-30, by haftmann
moved lemmas about sup on bool to Lattices.thy
2009-09-30, by haftmann
tuned proofs
2009-09-30, by haftmann
tuned headings
2009-09-30, by haftmann
report unreferenced ids;
2009-09-30, by wenzelm
tuned whitespace;
2009-09-30, by wenzelm
more uniform treatment of structure Unsynchronized in ML bootstrap phase;
2009-09-30, by wenzelm
merged
2009-09-30, by haftmann
mandatory prefix where appropriate
2009-09-30, by haftmann
mandatory prefix where appropriate
2009-09-30, by haftmann
tuned whitespace
2009-09-30, by haftmann
replaced chained_goal by slightly more appropriate flat_goal;
2009-09-30, by wenzelm
made SML/NJ happy;
2009-09-30, by wenzelm
added chained_goal, which presents the goal thm as seen by semi-structured methods;
2009-09-30, by wenzelm
tuned;
2009-09-29, by wenzelm
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
cleaned up abstract tuple operations and named them consistently
2009-07-29, by haftmann
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
2009-07-30, by wenzelm
trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
2009-07-30, by wenzelm
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
2009-07-30, by wenzelm
qualified Subgoal.FOCUS;
2009-07-30, by wenzelm
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
2009-07-30, by wenzelm
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
2009-07-30, by wenzelm
Variable.importT/import: return full instantiations, tuned;
2009-07-30, by wenzelm
added certify_inst, certify_instantiate;
2009-07-30, by wenzelm
merged
2009-07-29, by wenzelm
trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
2009-07-29, by wenzelm
proper Jinja-Slicing;
2009-07-29, by wenzelm
merged
2009-07-29, by wenzelm
merged
2009-07-29, by haftmann
abstractions: desymbolize name hint
2009-07-29, by haftmann
added numeral code postprocessor rules on type int
2009-07-29, by haftmann
sos comments modified
2009-07-29, by nipkow
sos documentation
2009-07-29, by nipkow
Added remote-SOS changes by Philipp Meyer
2009-07-29, by nipkow
Functionality for sum of squares to call a remote csdp prover
2009-07-24, by Philipp Meyer
merged
2009-07-28, by wenzelm
updated generated document
2009-07-28, by haftmann
reinserted legacy ML function
2009-07-28, by haftmann
Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-07-28, by haftmann
explicit is better than implicit
2009-07-28, by haftmann
Meson.first_order_resolve: avoid handle _;
2009-07-29, by wenzelm
removed old global get_claset/map_claset;
2009-07-29, by wenzelm
eliminated METAHYPS;
2009-07-28, by wenzelm
Future.shutdown before loading sequentially -- workaround scheduler deadlock;
2009-07-28, by wenzelm
ResAxioms.neg_conjecture_clauses: proper context;
2009-07-28, by wenzelm
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
2009-07-28, by wenzelm
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
2009-07-28, by wenzelm
eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-28, by wenzelm
non-critical use_thy;
2009-07-28, by wenzelm
future result: Synchronized.var;
2009-07-28, by wenzelm
added unsynchronized Synchronized.peek;
2009-07-28, by wenzelm
group status: Synchronized.var;
2009-07-28, by wenzelm
tuned;
2009-07-28, by wenzelm
Task_Queue.dequeue: explicit thread;
2009-07-28, by wenzelm
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
2009-07-28, by wenzelm
interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
2009-07-28, by wenzelm
misc tuning;
2009-07-28, by wenzelm
tuned
2009-07-28, by krauss
moved obsolete same_fst to Recdef.thy
2009-07-28, by krauss
adapted doc to type of "op O"
2009-07-28, by krauss
merged
2009-07-28, by wenzelm
merged
2009-07-27, by wenzelm
merged
2009-07-27, by wenzelm
merged
2009-07-27, by wenzelm
added proof of Kleene_Algebra.star_decomp
2009-07-27, by krauss
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
2009-07-27, by krauss
some lemmas about maps (contributed by Peter Lammich)
2009-07-27, by krauss
"more standard" argument order of relation composition (op O)
2009-07-27, by krauss
added rail antiquotation environment, which coexists with old-style content markup;
2009-07-28, by wenzelm
proper header;
2009-07-28, by wenzelm
proper context for SAT tactics;
2009-07-27, by wenzelm
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-27, by wenzelm
interruptible: Thread.testInterrupt before changing thread attributes;
2009-07-27, by wenzelm
wait: absorb spurious interrupts;
2009-07-27, by wenzelm
scheduler: shutdown spontaneously (after some delay) if queue is empty;
2009-07-27, by wenzelm
join_next: do not yield, even if overloaded, to minimize "running" tasks;
2009-07-27, by wenzelm
tuned tracing;
2009-07-27, by wenzelm
cancel: improved reactivity due to more careful broadcasting;
2009-07-27, by wenzelm
dequeue_towards: always return active tasks;
2009-07-27, by wenzelm
merged
2009-07-27, by wenzelm
removed unused low-level interrupts;
2009-07-27, by wenzelm
tuned signature;
2009-07-27, by wenzelm
tuned;
2009-07-27, by wenzelm
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
2009-07-27, by wenzelm
enqueue/finish: return minimal/maximal state of this task;
2009-07-27, by wenzelm
NEWS
2009-07-27, by haftmann
tacticals FOCUS and FOCUS_PARAMS;
2009-07-26, by wenzelm
replaced old METAHYPS by FOCUS;
2009-07-26, by wenzelm
replaced old METAHYPS by FOCUS;
2009-07-26, by wenzelm
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
2009-07-26, by wenzelm
replaced old METAHYPS by FOCUS;
2009-07-26, by wenzelm
tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
2009-07-26, by wenzelm
retrofit: actually handle schematic variables -- need to export into original context;
2009-07-26, by wenzelm
merged
2009-07-26, by wenzelm
adapted to changed prefixes
2009-07-26, by haftmann
merged
2009-07-26, by haftmann
improved handling of parameter import; tuned
2009-07-25, by haftmann
explicit is better than implicit
2009-07-25, by haftmann
localized interpretation of min/max-lattice
2009-07-25, by haftmann
adapted to localized interpretation of min/max-lattice
2009-07-25, by haftmann
SUBPROOF/Obtain.result: named params;
2009-07-26, by wenzelm
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
2009-07-26, by wenzelm
advanced retrofit, which allows new subgoals and variables;
2009-07-26, by wenzelm
Variable.focus: named parameters;
2009-07-26, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip