Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
NEWS
2004-12-18
schirmer
2004-12-18
added simproc for Let
file
|
diff
|
annotate
2004-12-13
nipkow
2004-12-13
*** empty log message ***
file
|
diff
|
annotate
2004-12-02
nipkow
2004-12-02
*** empty log message ***
file
|
diff
|
annotate
2004-12-01
nipkow
2004-12-01
*** empty log message ***
file
|
diff
|
annotate
2004-12-01
kleing
2004-12-01
new antiquotations @{lhs thm} and @{rhs thm}
file
|
diff
|
annotate
2004-11-24
nipkow
2004-11-24
*** empty log message ***
file
|
diff
|
annotate
2004-11-15
webertj
2004-11-15
minor rewording
file
|
diff
|
annotate
2004-11-12
webertj
2004-11-12
isatool usedir -f
file
|
diff
|
annotate
2004-10-12
nipkow
2004-10-12
*** empty log message ***
file
|
diff
|
annotate
2004-09-27
ballarin
2004-09-27
Modified locales: improved implementation of "includes".
file
|
diff
|
annotate
2004-09-13
nipkow
2004-09-13
*** empty log message ***
file
|
diff
|
annotate
2004-08-29
webertj
2004-08-29
Provers/blast.ML: depth_limit
file
|
diff
|
annotate
2004-08-23
webertj
2004-08-23
new isatool dimacs2hol
file
|
diff
|
annotate
2004-08-19
nipkow
2004-08-19
*** empty log message ***
file
|
diff
|
annotate
2004-08-16
nipkow
2004-08-16
*** empty log message ***
file
|
diff
|
annotate
2004-08-12
ballarin
2004-08-12
Disallowed "includes" in locale declarations.
file
|
diff
|
annotate
2004-08-06
nipkow
2004-08-06
undid UN/INT xsymbol syntax with subscripts.
file
|
diff
|
annotate
2004-08-03
ballarin
2004-08-03
New transitivity reasoners for transitivity only and quasi orders.
file
|
diff
|
annotate
2004-07-30
wenzelm
2004-07-30
ZF/Simplifier: second copy of context type solver;
file
|
diff
|
annotate
2004-07-26
ballarin
2004-07-26
New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
file
|
diff
|
annotate
2004-07-22
nipkow
2004-07-22
*** empty log message ***
file
|
diff
|
annotate
2004-07-15
nipkow
2004-07-15
*** empty log message ***
file
|
diff
|
annotate
2004-07-15
nipkow
2004-07-15
*** empty log message ***
file
|
diff
|
annotate
2004-07-15
nipkow
2004-07-15
*** empty log message ***
file
|
diff
|
annotate
2004-07-11
wenzelm
2004-07-11
Simplifier and Classical Reasoner now support proof context dependent plug-ins;
file
|
diff
|
annotate
2004-07-08
wenzelm
2004-07-08
tuned simprocs;
file
|
diff
|
annotate
2004-07-06
schirmer
2004-07-06
* Pure/Namespace: flag unique_names added * Pure/Tactic: print_tac outputs goal through trace channel * HOL/Simplifier: extended record_upd_simproc
file
|
diff
|
annotate
2004-06-30
schirmer
2004-06-30
Added reference record_definition_quick_and_dirty_sensitive, to skip proofs triggered by a record definition, if quick_and_dirty is enabled.
file
|
diff
|
annotate
2004-06-30
skalberg
2004-06-30
Made simplification procedures simpset-aware.
file
|
diff
|
annotate
2004-06-20
wenzelm
2004-06-20
tuned;
file
|
diff
|
annotate
2004-06-13
wenzelm
2004-06-13
added display_drafts and print_drafts commands;
file
|
diff
|
annotate
2004-06-10
wenzelm
2004-06-10
tuned;
file
|
diff
|
annotate
2004-06-10
wenzelm
2004-06-10
tuned;
file
|
diff
|
annotate
2004-06-09
wenzelm
2004-06-09
* Document preparation: antiquotations provide option 'locale=NAME';
file
|
diff
|
annotate
2004-06-08
paulson
2004-06-08
Groups, Rings and supporting lemmas in ZF
file
|
diff
|
annotate
2004-06-06
wenzelm
2004-06-06
HOL: symbolic syntax of Eps;
file
|
diff
|
annotate
2004-06-01
wenzelm
2004-06-01
removed obsolete sort 'logic';
file
|
diff
|
annotate
2004-05-29
wenzelm
2004-05-29
* ML: all output via channels of writeln etc. passed through Output.output;
file
|
diff
|
annotate
2004-05-21
wenzelm
2004-05-21
Pure: clear separation of logical types and nonterminals;
file
|
diff
|
annotate
2004-05-10
wenzelm
2004-05-10
Pure: nested comments in inner syntax;
file
|
diff
|
annotate
2004-05-06
schirmer
2004-05-06
tuned HOL/record package; enabled record_upd_simproc by default.
file
|
diff
|
annotate
2004-05-06
wenzelm
2004-05-06
show_structs option;
file
|
diff
|
annotate
2004-05-03
schirmer
2004-05-03
reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.
file
|
diff
|
annotate
2004-05-01
wenzelm
2004-05-01
tuned;
file
|
diff
|
annotate
2004-05-01
wenzelm
2004-05-01
improvd indexed syntax and implicit structures; tuned renaming of symbolic identifiers
file
|
diff
|
annotate
2004-04-29
wenzelm
2004-04-29
HOLCF: discontinued special version of 'constdefs';
file
|
diff
|
annotate
2004-04-22
wenzelm
2004-04-22
Pure: considerably improved version of 'constdefs' command; Pure: 'advanced' translation functions (parse_translation etc.);
file
|
diff
|
annotate
2004-04-19
kleing
2004-04-19
add HOL4
file
|
diff
|
annotate
2004-04-17
kleing
2004-04-17
added HOL-Matrix, added HOL/Matrix/ROOT.ML
file
|
diff
|
annotate
2004-04-16
wenzelm
2004-04-16
Pure: 'instance' now handles general arities;
file
|
diff
|
annotate
2004-04-16
berghofe
2004-04-16
Added entry for quickcheck command.
file
|
diff
|
annotate
2004-04-15
wenzelm
2004-04-15
tuned;
file
|
diff
|
annotate
2004-04-14
schirmer
2004-04-14
* raw control symbols are of the form \<^raw:...> now. * again allowing symbols to begin with "\\" instead of "\" for compatibility with ML-strings of old style theory and ML-files and isa-ProofGeneral.
file
|
diff
|
annotate
2004-04-13
wenzelm
2004-04-13
* Calculation commands "moreover" and "also" no longer interfere with current facts ("this"), admitting arbitrary combinations with "then" and derived forms.
file
|
diff
|
annotate
2004-04-13
ballarin
2004-04-13
Various changes to HOL-Algebra; Locale instantiation.
file
|
diff
|
annotate
2004-04-13
kleing
2004-04-13
isabelle.css
file
|
diff
|
annotate
2004-04-12
oheimb
2004-04-12
added HOLCF/Streams.thy (with concatenation etc.)
file
|
diff
|
annotate
2004-04-02
ballarin
2004-04-02
Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
file
|
diff
|
annotate
2004-03-31
skalberg
2004-03-31
Added check that Theory.ML does not occur in the files section of the theory Theory.
file
|
diff
|
annotate
2004-03-24
paulson
2004-03-24
clarified
file
|
diff
|
annotate