Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
switched import from Main to PreList
2007-12-10, by haftmann
explicit import of theory ATP_Linkup
2007-12-10, by haftmann
explicit import of theory Main
2007-12-10, by haftmann
swtiched ATP_Linkup and PreList in theory hierarchy
2007-12-10, by haftmann
ML_OPTIONS="-H 1500" -- potentially works around GC core dump;
2007-12-09, by wenzelm
added Id, some cleanup
2007-12-09, by krauss
tuned message;
2007-12-08, by wenzelm
renamed IsabelleResult to IsabelleProcess.Result;
2007-12-08, by wenzelm
Isabelle process wrapper for JVM platform (tentative implementation in
2007-12-08, by wenzelm
tuned messages;
2007-12-08, by wenzelm
Isar loop: recover after toplevel crashes;
2007-12-08, by wenzelm
secure_main: enforces terminator, to gain robustness;
2007-12-08, by wenzelm
text_of: make double sure that result is well-formed, to avoid recurrent failures;
2007-12-08, by wenzelm
ML_OPTIONS="-H 1000" -- potentially works around GC core dump;
2007-12-08, by wenzelm
added off-line parse;
2007-12-07, by wenzelm
(alt)string: allow explicit character codes (as in ML);
2007-12-07, by wenzelm
added nested 'Isabelle.command';
2007-12-07, by wenzelm
updated;
2007-12-07, by wenzelm
special_end: replaced Z by dot;
2007-12-07, by wenzelm
output_prompt: CRITICAL;
2007-12-07, by wenzelm
declaration of instance parameter names
2007-12-07, by haftmann
exported declare_names
2007-12-07, by haftmann
new primrec
2007-12-07, by haftmann
instantiation target rather than legacy instance
2007-12-07, by haftmann
proper treatment of code theorems for primrec
2007-12-07, by haftmann
dropped Instance.instantiate
2007-12-07, by haftmann
Adding "ex/Induction_Scheme.thy" to tests
2007-12-07, by krauss
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
2007-12-07, by krauss
tuned further
2007-12-07, by haftmann
renamed ML_PID to PID;
2007-12-06, by wenzelm
R&F: added sgn lemma
2007-12-06, by nipkow
temporary code generator work arounds
2007-12-06, by haftmann
fixed slip
2007-12-06, by haftmann
-authentic primrec
2007-12-06, by haftmann
dropped legacy bindings
2007-12-06, by haftmann
authentic primrec
2007-12-06, by haftmann
dropped void space
2007-12-06, by haftmann
added new primrec package
2007-12-06, by haftmann
load sum_tree.ML
2007-12-06, by krauss
factored out handling of sum types again
2007-12-06, by krauss
added test_markup;
2007-12-06, by wenzelm
moved basic test_markup to isabelle_process.ML;
2007-12-06, by wenzelm
added channels;
2007-12-06, by wenzelm
replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
2007-12-06, by wenzelm
check persistent sessions;
2007-12-06, by wenzelm
tuned signature;
2007-12-05, by wenzelm
made SML/NJ happy;
2007-12-05, by wenzelm
removed -e flag from most sessions;
2007-12-05, by wenzelm
instance int,real :: lordered_ring
2007-12-05, by obua
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
2007-12-05, by krauss
tuned class parts
2007-12-05, by haftmann
dropped Classpackage.thy
2007-12-05, by haftmann
tuned
2007-12-05, by haftmann
added parser for multi_arity
2007-12-05, by haftmann
added constrain_thm
2007-12-05, by haftmann
canonical instantiation
2007-12-05, by haftmann
map_product and fold_product
2007-12-05, by haftmann
interface and distinct simproc tuned
2007-12-05, by haftmann
improved
2007-12-05, by haftmann
interpretation of typedefs
2007-12-05, by haftmann
simplified infrastructure for code generator operational equality
2007-12-05, by haftmann
added something about instantiation target
2007-12-05, by haftmann
switch poly to 5.1, removed -e flag from most sessions
2007-12-05, by kleing
switch at-poly main to poly 5.1
2007-12-05, by kleing
make mac-poly non-experimental
2007-12-05, by kleing
make at64 non-experimental
2007-12-05, by kleing
Isabelle process wrapper -- interaction via external program.
2007-12-04, by wenzelm
Toplevel.loop: explicit argument for secure loop, no warning on quit;
2007-12-04, by wenzelm
added Isar.secure_main;
2007-12-04, by wenzelm
added Tools/isabelle_process.ML;
2007-12-04, by wenzelm
isabelle process: replaced option -p by -W (process wrapper);
2007-12-04, by wenzelm
replaced option -p by -W (process wrapper);
2007-12-04, by wenzelm
\<chi> is now considered a letter;
2007-12-04, by wenzelm
symbol chi is also a letter;
2007-12-04, by wenzelm
improvements
2007-12-03, by obua
overloading target
2007-12-03, by haftmann
interface for unchecked definitions
2007-12-03, by haftmann
shifted "fun" command to Wellfounded_Relations
2007-12-03, by haftmann
updated
2007-12-03, by haftmann
Eliminated unused theorems minusinf_ex and minusinf_bex
2007-12-02, by chaieb
first working version of instance target
2007-11-30, by haftmann
interpretation for typedefs
2007-11-30, by haftmann
using intro_locales instead of unfold_locales if appropriate
2007-11-30, by haftmann
more canonical attribute application
2007-11-30, by haftmann
adjustions to due to instance target
2007-11-30, by haftmann
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
2007-11-30, by krauss
*** empty log message ***
2007-11-30, by nipkow
added {#.,.,...#}
2007-11-30, by nipkow
tuned
2007-11-29, by haftmann
stripped down
2007-11-29, by haftmann
isabelle-process: option -p echos ISABELLE_PID;
2007-11-29, by wenzelm
commit: non-critical, otherwise session restart will result in deadlock!
2007-11-29, by wenzelm
instance command as rudimentary class target
2007-11-29, by haftmann
dropped dead code
2007-11-29, by haftmann
polyml: default heap size is back to -H 200 (people are still using
2007-11-28, by wenzelm
an example file for how to treat Felleisen-Hieb-style contexts
2007-11-28, by urbanc
removed (cf. object_logic.ML);
2007-11-28, by wenzelm
added base_sort;
2007-11-28, by wenzelm
removed typedecl.ML (cf. object_logic.ML);
2007-11-28, by wenzelm
ObjectLogic.typedecl;
2007-11-28, by wenzelm
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
2007-11-28, by wenzelm
simplified using sledgehammer
2007-11-28, by paulson
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
2007-11-28, by paulson
comment
2007-11-28, by paulson
(reverted to unnamed infix)
2007-11-28, by haftmann
simplified interpretations
2007-11-28, by haftmann
deleted looping code theorem
2007-11-28, by haftmann
to_set now applies collect_mem_simproc as well.
2007-11-28, by berghofe
naming policy for instances
2007-11-28, by haftmann
tuned interfaces of class module
2007-11-28, by haftmann
dropped dead code
2007-11-28, by haftmann
dropped legacy unnamed infix
2007-11-28, by haftmann
dropped implicit assumption proof
2007-11-28, by haftmann
dropped legacy ml bindings
2007-11-28, by haftmann
tuned titles;
2007-11-27, by wenzelm
moved titles;
2007-11-27, by wenzelm
tuned title;
2007-11-27, by wenzelm
tuned titles;
2007-11-27, by wenzelm
standard_parse_term: check ambiguous results without changing the result yet;
2007-11-27, by wenzelm
challenge by John Harrison: down to 12s (was 17s, was 75s);
2007-11-27, by wenzelm
Knaster_Tarski: turned into Isar statement, tuned proofs;
2007-11-27, by wenzelm
first_order_match now only calls loose_bvar when inside an abstraction.
2007-11-27, by berghofe
check_conv now only performs beta-eta-normalization when equations
2007-11-27, by berghofe
Optimized beta_norm: only tries to normalize term when it contains
2007-11-27, by berghofe
Better error messages for cterm_instantiate.
2007-11-27, by berghofe
some more lemmas due to Peter Lammich;
2007-11-26, by wenzelm
Peter Lammich: HOL-Lattice lemmas;
2007-11-26, by wenzelm
Removed forced roman font in mode=IfThen.
2007-11-26, by nipkow
use official polyml-5.1;
2007-11-26, by wenzelm
tuned comments;
2007-11-26, by wenzelm
moved new NEWS from Isabelle2007 to this Isabelle version'';
2007-11-26, by wenzelm
simplified website rsync
2007-11-26, by haftmann
rudimentary instantiation target
2007-11-23, by haftmann
explicit type signature
2007-11-23, by haftmann
interpretation of typedecls: instantiation to class type
2007-11-23, by haftmann
deleted card definition as code lemma; authentic syntax for card
2007-11-23, by haftmann
separated typedecl module, providing typedecl command with interpretation
2007-11-23, by haftmann
faster metis calls
2007-11-23, by paulson
tuned;
Isabelle2007
2007-11-22, by wenzelm
updated to official Poly/ML 5.1;
2007-11-22, by wenzelm
tuned;
2007-11-21, by wenzelm
include elapsed time for parallel sessions;
2007-11-21, by wenzelm
intern_skolem: disallow qualified names;
2007-11-21, by wenzelm
fixed
2007-11-21, by haftmann
dropped diagnostic commands
2007-11-21, by haftmann
tuned;
2007-11-20, by wenzelm
tuned spacing;
2007-11-20, by wenzelm
updated Proof General advertisement;
2007-11-20, by wenzelm
PolyML.SaveState.loadState: exit on failure;
2007-11-20, by wenzelm
Init outer syntax after message setup to avoid spurious output.
2007-11-19, by aspinall
update to most recent smlnj version
2007-11-19, by isatest
inform_file_processed: made even more robust against bad file specs;
2007-11-19, by wenzelm
removed unused inform_file_processed;
2007-11-18, by wenzelm
init_empty: check before change (avoids non-linear update);
2007-11-18, by wenzelm
Add thm_dep preference to menu, inadvertently missed off
2007-11-15, by aspinall
tuned;
2007-11-15, by wenzelm
use -source instead of -target;
2007-11-15, by wenzelm
target 1.4 of JVM;
2007-11-15, by wenzelm
thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
2007-11-15, by wenzelm
isatool version: clarify that this is the *long* form;
2007-11-15, by wenzelm
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
2007-11-15, by wenzelm
cover ISABELLE_IDENTIFIER;
2007-11-15, by wenzelm
README for E binary distribution;
2007-11-14, by wenzelm
tuned;
2007-11-14, by wenzelm
patching in the latest changes from Hurd
2007-11-13, by paulson
tuned;
2007-11-13, by wenzelm
some more items;
2007-11-13, by wenzelm
updated
2007-11-13, by nipkow
Added JAR paper by Wenzel and Wiedijk.
2007-11-13, by berghofe
Removed some case_names and consumes attributes that are now no longer
2007-11-13, by berghofe
Added TrueE to extraction_expand.
2007-11-13, by berghofe
Added new program extraction examples.
2007-11-13, by berghofe
New case studies for program extraction.
2007-11-13, by berghofe
Moved auxiliary lemmas to separate theory.
2007-11-13, by berghofe
Added new exampes Greatest_Common_Divisor and Euclid.
2007-11-13, by berghofe
Moved nat_eq_dec to Util.thy
2007-11-13, by berghofe
Moved nat_eq_dec and search to Util.thy
2007-11-13, by berghofe
Tuned.
2007-11-13, by berghofe
to_pred and to_set now save induction and case rule tags.
2007-11-13, by berghofe
removed left-over text links from lynx conversion;
2007-11-12, by wenzelm
back to sigusr2, after Poly/ML 5.1 has been adapted;
2007-11-12, by wenzelm
changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
2007-11-12, by wenzelm
updates
2007-11-12, by nipkow
updated
2007-11-12, by haftmann
reactivated default paragraph formatting for ``proof documents'';
2007-11-12, by wenzelm
fixed typo;
2007-11-12, by schirmer
added signatures;
2007-11-12, by schirmer
abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
updates
2007-11-11, by nipkow
avoid ML print in production code;
2007-11-11, by wenzelm
updated;
2007-11-11, by wenzelm
auto quickcheck: reduced messages;
2007-11-11, by wenzelm
notation works with any known constant (including fixes/abbrevs);
2007-11-11, by wenzelm
HOL-Statespace;
2007-11-11, by wenzelm
* HOL-Statespace;
2007-11-11, by wenzelm
restore interrupt handler on init;
2007-11-11, by wenzelm
abbrev: back to PrintMode.internal, which works at least half-way;
2007-11-11, by wenzelm
syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11, by wenzelm
replaced extend_prtabs by update_prtabs (absorb duplicates);
2007-11-11, by wenzelm
abbrev: PrintMode.input instead of PrintMode.internal for global version!
2007-11-11, by wenzelm
renamed update_list to cons_list;
2007-11-11, by wenzelm
syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11, by wenzelm
renamed Symtab.update_list to Symtab.cons_list;
2007-11-11, by wenzelm
tuned specifications of 'notation';
2007-11-11, by wenzelm
added update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
remove_prtabs: tuned, avoid excessive garbage;
2007-11-10, by wenzelm
update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
similar_types: uniform treatment of TFrees/TVars;
2007-11-10, by wenzelm
notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
tuned specifications of 'notation';
2007-11-10, by wenzelm
removed LocalTheory.target_naming/name;
2007-11-10, by wenzelm
put_inductives: be permissive about multiple versions
2007-11-10, by wenzelm
tuned proofs;
2007-11-10, by wenzelm
tuned document;
2007-11-10, by wenzelm
Orderings.min/max: no need to qualify consts;
2007-11-10, by wenzelm
auto_quickcheck ref: set default in ProofGeneral/preferences only
2007-11-10, by wenzelm
ProofGeneral/preferences: auto_quickcheck=true;
2007-11-10, by wenzelm
qualified Proofterm.proofs;
2007-11-10, by wenzelm
@{const}: improved ProofContext.read_const does the job;
2007-11-10, by wenzelm
locale_const: suppress in class body as well (prevents qualified printing);
2007-11-10, by wenzelm
notation: improved ProofContext.read_const does the job;
2007-11-10, by wenzelm
updated;
2007-11-10, by wenzelm
replaced @{const} (allows name only) by proper @{term};
2007-11-10, by wenzelm
proper implementation of check phase; non-qualified names for class operations
2007-11-09, by haftmann
explicit message for failed autoquickcheck
2007-11-09, by haftmann
tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-09, by wenzelm
avoid obsolete Sign.read_prop;
2007-11-09, by wenzelm
tuned proofs -- avoid implicit prems;
2007-11-09, by wenzelm
fixed imports path;
2007-11-09, by wenzelm
tuned proofs -- avoid open cases;
2007-11-09, by wenzelm
function package: using the names of the equations as case names turned out to be impractical => disabled
2007-11-09, by krauss
avoid name clashes when generating code for union, inter
2007-11-09, by krauss
oops -- avoid vacous goal message;
2007-11-08, by wenzelm
tuned messages;
2007-11-08, by wenzelm
avoid "import" as identifier, which is a keyword in Alice;
2007-11-08, by wenzelm
tuned presentation;
2007-11-08, by wenzelm
avoid implicit use of prems;
2007-11-08, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip