Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+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.
wrap line correctly in Nitpick documentation
2009-10-22, by blanchet
added Nitpick's theory and ML files to Isabelle/HOL;
2009-10-22, by blanchet
Added Nitpick manual.
2009-10-22, by blanchet
merged
2009-10-26, by berghofe
Added Pattern.thy to Nominal/Examples.
2009-10-26, by berghofe
merged
2009-10-26, by haftmann
tuned
2009-10-26, by haftmann
added SML_Quickcheck import
2009-10-26, by haftmann
tuned code setup for primitive boolean connectors
2009-10-26, by haftmann
legacy warnings for old-style term styles
2009-10-26, by haftmann
removed unnecessary NameSpace prefix;
2009-10-26, by wenzelm
misc tuning and updates;
2009-10-26, by wenzelm
merged
2009-10-26, by wenzelm
implicit default is 4 cores -- more cost-effective;
2009-10-26, by wenzelm
deleted junk;
2009-10-26, by wenzelm
more precise dependencies, notably for HOL-Multivariate_Analysis;
2009-10-26, by wenzelm
re-moved theory Fin_Fun to AFP
2009-10-26, by haftmann
merged
2009-10-26, by haftmann
distinguished session for multivariate analysis
2009-10-23, by himmelma
adjusted to changes in corresponding ML code
2009-10-26, by haftmann
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25, by wenzelm
maintain theory name via name space, not tags;
2009-10-25, by wenzelm
name space groups are identified by serial, not serial_string;
2009-10-25, by wenzelm
maintain group via name space, not tags;
2009-10-25, by wenzelm
LocalTheory.naming_of;
2009-10-25, by wenzelm
begin_theory: set theory_name here;
2009-10-25, by wenzelm
maintain group via name space, not tags;
2009-10-25, by wenzelm
maintain proper Name_Space.naming, with conceal and set_group;
2009-10-25, by wenzelm
more direct access to naming;
2009-10-25, by wenzelm
Name_Space.naming: maintain group and theory_name as well;
2009-10-25, by wenzelm
export is_concealed;
2009-10-25, by wenzelm
merge_list: no exception DUP here;
2009-10-25, by wenzelm
merged
2009-10-25, by wenzelm
more uniform ISABELLE_USEDIR_OPTIONS;
2009-10-25, by wenzelm
make SML/NJ happy;
2009-10-25, by wenzelm
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip