Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
added setmp_thread_data_seq;
2008-01-24, by wenzelm
removed obsolete context_position.ML (superseded by Position.thread_data);
2008-01-24, by wenzelm
switched to polyml-cvs;
2008-01-24, by wenzelm
Reimplemented proof of strong induction theorem.
2008-01-24, by berghofe
Added lemma at_fin_set_fresh.
2008-01-24, by berghofe
reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;
2008-01-23, by wenzelm
exceptions: assign result = null properly;
2008-01-23, by wenzelm
tuned proofs;
2008-01-23, by wenzelm
recovered #der example without using val it;
2008-01-23, by wenzelm
yet another OCaml fix
2008-01-23, by haftmann
tuned
2008-01-22, by haftmann
added map_split
2008-01-22, by haftmann
added class semiring_div
2008-01-22, by haftmann
fixed OCaml
2008-01-22, by haftmann
avoid 'it' in ML expressions
2008-01-22, by haftmann
Removed Logic.auto_rename.
2008-01-21, by berghofe
Efficient_Nat streamlined and improved
2008-01-21, by haftmann
tuned proof
2008-01-21, by haftmann
non-negative numerals
2008-01-21, by haftmann
tuned
2008-01-21, by haftmann
more lemmas
2008-01-21, by haftmann
proper meaningful examples
2008-01-21, by haftmann
explicit auxiliary function for code setup
2008-01-21, by haftmann
streamlined and improved
2008-01-21, by haftmann
adjusted to constant and theorem renames
2008-01-21, by haftmann
avoiding direct references to numeral presentation
2008-01-21, by haftmann
tuned code setup
2008-01-21, by haftmann
add space to binder syntax
2008-01-18, by huffman
pcpodef generates strict_iff lemmas
2008-01-18, by huffman
change lemma admD to rule_format
2008-01-18, by huffman
improved implementation
2008-01-18, by haftmann
convert lemma lub_mono to rule_format
2008-01-17, by huffman
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
2008-01-17, by huffman
change class axiom chfin to rule_format
2008-01-17, by huffman
change class axiom ax_flat to rule_format
2008-01-16, by huffman
joined theories IntDef, Numeral, IntArith to theory Int
2008-01-15, by haftmann
tuned
2008-01-15, by haftmann
further localization
2008-01-15, by haftmann
explicit code lemma for implication
2008-01-15, by haftmann
add instance for class bifinite
2008-01-15, by huffman
clean up some proofs;
2008-01-15, by huffman
declare cpair_strict [simp]
2008-01-15, by huffman
make at-sml-dev experimental
2008-01-14, by isatest
added bifinite class instance
2008-01-14, by huffman
add bifinite instances
2008-01-14, by huffman
add class bifinite_cpo for possibly-unpointed bifinite domains
2008-01-14, by huffman
cleaned up instance proofs
2008-01-14, by huffman
new-style instantiation proof for unit :: po
2008-01-14, by huffman
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
2008-01-14, by huffman
simplified chfin instance proof
2008-01-14, by huffman
new theory of powerdomains
2008-01-14, by huffman
new theory of bifinite domains
2008-01-14, by huffman
new-style class instantiation
2008-01-14, by huffman
added lemmas lub_distribs
2008-01-14, by huffman
*** empty log message ***
2008-01-14, by nipkow
*** empty log message ***
2008-01-14, by nipkow
compact_chfin is now declared simp
2008-01-14, by huffman
use new-style class for po
2008-01-14, by huffman
add lemma contI2
2008-01-14, by huffman
converted adm_all and adm_ball to rule_format; cleaned up
2008-01-14, by huffman
Equations for constants without arguments are now declared using
2008-01-13, by berghofe
new theory defining set as a pcpo
2008-01-10, by huffman
Test data generation and conversion to terms are now more closely
2008-01-10, by berghofe
New example involving functions.
2008-01-10, by berghofe
Now uses more carefully designed simpsets to prevent proofs from
2008-01-10, by berghofe
Test data generation and conversion to terms is now more closely
2008-01-10, by berghofe
Eliminated DatatypeAux.dest_TFree to avoid clashes
2008-01-10, by berghofe
Added nil_const and cons_const.
2008-01-10, by berghofe
Added test data generator for function type (from Pure/codegen.ML).
2008-01-10, by berghofe
New interface for test data generators.
2008-01-10, by berghofe
declare ch2ch_LAM [simp]
2008-01-10, by huffman
added overloading target
2008-01-10, by haftmann
new compactness lemmas; removed duplicated flat_less_iff
2008-01-10, by huffman
Compactness subsection with new lemmas
2008-01-10, by huffman
Compactness subsection with some new lemmas
2008-01-10, by huffman
new compactness lemmas
2008-01-10, by huffman
new lemmas max_in_chainI, max_in_chainD
2008-01-10, by huffman
overloading target
2008-01-09, by haftmann
tuned
2008-01-09, by nipkow
added simp attributes/ proofs fixed
2008-01-09, by nipkow
added simp attributes
2008-01-09, by nipkow
Finally: no more unproven.
2008-01-09, by nipkow
tuned
2008-01-09, by haftmann
some more primrec
2008-01-09, by haftmann
tuned
2008-01-09, by haftmann
a note on syntax in class context
2008-01-09, by haftmann
a note on syntax
2008-01-09, by haftmann
tuned proofs
2008-01-08, by urbanc
normalization conversion
2008-01-08, by haftmann
tuned comment
2008-01-08, by haftmann
explicit type variables for instantiation
2008-01-08, by haftmann
better error reporting
2008-01-08, by haftmann
tuned
2008-01-08, by haftmann
refined overloading target
2008-01-08, by haftmann
imp_conv_disj is now declared as a "code unfold" lemma to avoid that
2008-01-08, by berghofe
isabelle.jars: temporarily disabled, until isatest gets up-to-date java;
2008-01-07, by wenzelm
some pre-release tunings
2008-01-07, by urbanc
more robust console thread (cf. jedit plugin version);
2008-01-06, by wenzelm
build Isabelle process wrapper;
2008-01-06, by wenzelm
* Rudimentary Isabelle plugin for jEdit;
2008-01-06, by wenzelm
added plugin installation;
2008-01-06, by wenzelm
tuned;
2008-01-06, by wenzelm
purge build directory;
2008-01-06, by wenzelm
basic setup for Isabelle/jEdit plugin;
2008-01-06, by wenzelm
added interface for command-line option;
2008-01-06, by wenzelm
removed obsolete prompt and channel markups;
2008-01-06, by wenzelm
replaced prompt markup by prompt channel setup;
2008-01-06, by wenzelm
removed obsolete prompt markup;
2008-01-06, by wenzelm
removed unused of_stream;
2008-01-06, by wenzelm
added explicit prompt channel (prompt_fn/prompt);
2008-01-06, by wenzelm
removed obsolete prompt and channel markups;
2008-01-06, by wenzelm
Tuned relevant premises selection
2008-01-05, by chaieb
tuned comments;
2008-01-05, by wenzelm
added symbol output mode, with XML escapes;
2008-01-05, by wenzelm
export session id;
2008-01-05, by wenzelm
secure_main: removed separate welcome;
2008-01-05, by wenzelm
removed unused text_charref, cdata;
2008-01-05, by wenzelm
added INIT message, with pid and session property;
2008-01-05, by wenzelm
more instantiation
2008-01-05, by haftmann
adhering to instantiation policy
2008-01-05, by haftmann
cleaned up some proofs
2008-01-04, by huffman
simplified some proofs
2008-01-04, by huffman
partially adapted to new inversion rules
2008-01-04, by urbanc
adapted to new inversion rules
2008-01-04, by urbanc
fixed typo
2008-01-04, by haftmann
improved warning
2008-01-04, by haftmann
add new is_ub lemmas; clean up directed_finite proofs
2008-01-04, by huffman
new instance proofs for classes finite_po, chfin, flat
2008-01-04, by huffman
new lemma flat_less_iff
2008-01-03, by huffman
generalized chfindom_monofun2cont
2008-01-03, by huffman
Implemented proof of strong case analysis rule.
2008-01-03, by berghofe
Added function fresh_const.
2008-01-03, by berghofe
Added function partition_rules'.
2008-01-03, by berghofe
another attempt to disable documents;
2008-01-03, by wenzelm
simplified position_props, always include line/file fields;
2008-01-03, by wenzelm
replaced thread_properties by simplified version in position.ML;
2008-01-03, by wenzelm
nested_command: simplified properties vs. position -- the latter also includes id now;
2008-01-03, by wenzelm
type T: based on properties, added id field;
2008-01-03, by wenzelm
moved id to position properties;
2008-01-03, by wenzelm
instance unit :: finite_po
2008-01-03, by huffman
new axclass finite_po < finite, po
2008-01-03, by huffman
add lub_maximal lemmas;
2008-01-03, by huffman
added class Property: basic Isabelle properties;
2008-01-03, by wenzelm
tuned relevance test for presburger
2008-01-03, by chaieb
output message properties: id or position;
2008-01-03, by wenzelm
toplevel print_exn: proper setmp_thread_properties;
2008-01-03, by wenzelm
added id property;
2008-01-03, by wenzelm
Result: added props field;
2008-01-03, by wenzelm
remove legacy ML bindings
2008-01-03, by huffman
new-style theorem references
2008-01-03, by huffman
fix theorem references
2008-01-03, by huffman
generalized and simplified proof of adm_Finite
2008-01-03, by huffman
new lemma adm_upward
2008-01-03, by huffman
Tuned (type information in Lemmas)
2008-01-03, by chaieb
Changed order of tactics in presburger --- thinning before case splits
2008-01-03, by chaieb
maintain thread transition properties;
2008-01-03, by wenzelm
setmp_thread_data;
2008-01-03, by wenzelm
added setmp_thread_data;
2008-01-03, by wenzelm
type transition: added properties field;
2008-01-02, by wenzelm
added properties;
2008-01-02, by wenzelm
Isabelle.command: IsarCmd.nested_command (with properties);
2008-01-02, by wenzelm
added nested_command (with explicit position argument via properties);
2008-01-02, by wenzelm
of_properties: return filtered result;
2008-01-02, by wenzelm
added method encodeProperties;
2008-01-02, by wenzelm
setting -H 2000 and no documents for higher performance;
2008-01-02, by wenzelm
add dcpo instance proof
2008-01-02, by huffman
declare upE as cases rule; add new rule up_induct
2008-01-02, by huffman
update sq_ord/po instance proofs
2008-01-02, by huffman
move lemmas from Cont.thy to Ffun.thy;
2008-01-02, by huffman
remove not_up_less_UU [simp]
2008-01-02, by huffman
update instance proofs for sq_ord, po; new instance proofs for dcpo
2008-01-02, by huffman
add lemma ub2ub_monofun'
2008-01-02, by huffman
added dcpo instance proofs
2008-01-02, by huffman
new class dcpo; added dcpo versions of some lemmas
2008-01-02, by huffman
added new lemmas
2008-01-02, by huffman
add lemma dir2dir_monofun
2008-01-02, by huffman
tuned;
2008-01-02, by wenzelm
new is_ub lemmas; new lub syntax for set image
2008-01-02, by huffman
Multithreading.max_threads := 0 refers to number of cores of underlying machine;
2008-01-02, by wenzelm
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
2008-01-02, by wenzelm
added usedir -M max (alias for -M 0);
2008-01-02, by wenzelm
new section for directed sets
2008-01-02, by huffman
split of class uminus
2008-01-02, by haftmann
empty dictionaries for OCaml
2008-01-02, by haftmann
clarified policy
2008-01-02, by haftmann
tuned
2008-01-02, by haftmann
some more antiquotations
2008-01-02, by haftmann
index now a copy of nat rather than int
2008-01-02, by haftmann
absolute import
2008-01-02, by haftmann
some more primrec
2008-01-02, by haftmann
removed some legacy instantiations
2008-01-02, by haftmann
improved evaluation mechanism
2008-01-02, by haftmann
splitted class uminus from class minus
2008-01-02, by haftmann
testing for empty sort
2008-01-02, by paulson
new metis proofs
2008-01-02, by paulson
renamed foldM to fold_mset on general request
2008-01-02, by kleing
update instance proofs to new style
2008-01-02, by huffman
declare sprodE as cases rule; new induction rule sprod_induct
2008-01-01, by huffman
add induction rule ssum_induct
2008-01-01, by huffman
eval_wrapper: CRITICAL;
2008-01-01, by wenzelm
try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;
2008-01-01, by wenzelm
tuned spaces;
2008-01-01, by wenzelm
removed separate exists/forall code;
2008-01-01, by wenzelm
tuned proofs and comments
2008-01-01, by urbanc
removed obsolete banner;
2007-12-31, by wenzelm
tuned;
2007-12-30, by wenzelm
added PROMPT message;
2007-12-30, by wenzelm
added isSystem;
2007-12-30, by wenzelm
simple make script;
2007-12-30, by wenzelm
tuned comments (javadoc);
2007-12-29, by wenzelm
use polyml-cvs, the 5.2 development branch;
2007-12-27, by wenzelm
tuned RandomWord interface;
2007-12-22, by wenzelm
added int/real/list operations;
2007-12-22, by wenzelm
use random_word.ML earlier;
2007-12-22, by wenzelm
changed type definition to make Iwhen and reasoning about chains unnecessary;
2007-12-21, by huffman
Fixed eta constraction issue in compose_witness
2007-12-21, by ballarin
included meson/metis tests in simultaneous use_thys;
2007-12-20, by wenzelm
``print mode'' is now a thread-local value derived from a global template;
2007-12-20, by wenzelm
scheduling/next_task: PrintMode.closure;
2007-12-20, by wenzelm
added get/put_data;
2007-12-20, by wenzelm
separated into global template vs. thread-local value;
2007-12-20, by wenzelm
Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
2007-12-20, by wenzelm
added ML-Systems/universal.ML;
2007-12-20, by wenzelm
updated;
2007-12-20, by wenzelm
obsolete;
2007-12-20, by wenzelm
removed obsolete (slow!) Random implementation;
2007-12-20, by wenzelm
moved Pure/General/random_word.ML to Tools/random_word.ML;
2007-12-20, by wenzelm
adapted theory name;
2007-12-20, by wenzelm
* Metis prover an order of magnitude faster, works with multithreading.
2007-12-20, by wenzelm
updated HOL-Nominal-Examples deps;
2007-12-20, by wenzelm
made refute non-critical (seems to work after avoiding floating point random numbers);
2007-12-20, by wenzelm
move bottom-related stuff back into Pcpo.thy
2007-12-20, by huffman
polishing of some proofs
2007-12-20, by urbanc
Random.range_real makes SML/NJ happy;
2007-12-20, by wenzelm
tuned comments;
2007-12-19, by wenzelm
tuned RandomWord signature;
2007-12-19, by wenzelm
removed strange MacRoman character;
2007-12-19, by wenzelm
using RandomWord from Isabelle/Pure gains factor 10-20 speedup;
2007-12-19, by wenzelm
updated;
2007-12-19, by wenzelm
added General/random_word.ML;
2007-12-19, by wenzelm
Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
2007-12-19, by wenzelm
removed duplicate CRITICAL markup;
2007-12-19, by wenzelm
instantiation target
2007-12-19, by haftmann
tuned primitive inferences
2007-12-19, by haftmann
Replaced refs by config params; finer critical section in mets method
2007-12-19, by paulson
simultaneous use_thys;
2007-12-19, by wenzelm
marked refute (the main metis procedure) as CRITICAL;
2007-12-19, by wenzelm
more examples
2007-12-19, by schirmer
accomodate to replacement of K_record by %x.c
2007-12-19, by schirmer
replaced K_record by lambda term %x. c
2007-12-19, by schirmer
signature BASIC_MULTITHREADING;
2007-12-18, by wenzelm
removed obsolete use_noncritical (plain use is already non-critical);
2007-12-18, by wenzelm
serial: now based on specific version in structure Multithreading;
2007-12-18, by wenzelm
add class ppo of pointed partial orders;
2007-12-18, by huffman
named some critical sections;
2007-12-18, by wenzelm
named some critical sections;
2007-12-18, by wenzelm
use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
2007-12-18, by wenzelm
non-critical (accidental concurrent access does not affect functional integrity);
2007-12-18, by wenzelm
PrintMode.setmp (avoid direct access to print_mode ref);
2007-12-18, by wenzelm
rearrange into subsections
2007-12-18, by huffman
Skolemization now catches exception THM, which may be raised if unification fails.
2007-12-18, by paulson
Deleted redundant setmp calls
2007-12-18, by paulson
tuned proofs, document;
2007-12-18, by wenzelm
switched from PreList to ATP_Linkup
2007-12-18, by haftmann
Renamed *.size to prod.size.
2007-12-18, by berghofe
Alternative names are now also used when storing theorems for
2007-12-18, by berghofe
temporarily fixed documentation due to changed size functions
2007-12-18, by krauss
split_primel: salvaged original proof after blow with sledghammer
2007-12-18, by wenzelm
cond_timeit: added message argument, use Exn.capture/release;
2007-12-17, by wenzelm
cond_timeit: added message argument;
2007-12-17, by wenzelm
note in target
2007-12-17, by haftmann
maior tuning
2007-12-17, by haftmann
tuned
2007-12-17, by haftmann
Added foldl1.
2007-12-17, by berghofe
Adapted to changes in size function.
2007-12-17, by berghofe
size functions for nested datatypes are now expressed using
2007-12-17, by berghofe
Adapted to changes in interface of indtac.
2007-12-17, by berghofe
- Removed redundant head_len field in datatype_info
2007-12-17, by berghofe
- Removed redundant head_len field in datatype_info
2007-12-17, by berghofe
tidied some messy proofs
2007-12-17, by paulson
Deleted copy of indtac.
2007-12-17, by berghofe
Added code lemma for message_string_size.
2007-12-17, by berghofe
Removed obsolete lemma size_sum.
2007-12-17, by berghofe
fixed ancestors
2007-12-17, by paulson
whitespace typo
2007-12-17, by haftmann
explicit closing of derived witnesses
2007-12-17, by haftmann
closed rules
2007-12-17, by haftmann
improved semantics of timeapp_msg
2007-12-17, by haftmann
improved term syntax
2007-12-17, by haftmann
removed legacy proofs
2007-12-17, by nipkow
spread NEWS about "induction_scheme" method
2007-12-17, by krauss
settings for cvs version of poly
2007-12-16, by kleing
tuned comments;
2007-12-16, by wenzelm
constructor: allow default logic;
2007-12-16, by wenzelm
constructor: allow default logic;
2007-12-16, by wenzelm
tuned whitespace;
2007-12-15, by wenzelm
compose command line according to isabelle.shell/home system properties;
2007-12-15, by wenzelm
tuned comments;
2007-12-15, by wenzelm
addClassPath;
2007-12-15, by wenzelm
added example session with Beanshell;
2007-12-15, by wenzelm
ExitThread: deliver message before EXIT;
2007-12-15, by wenzelm
tuned;
2007-12-15, by wenzelm
tuned;
2007-12-15, by wenzelm
* isatool browser now works with Cygwin;
2007-12-15, by wenzelm
added javapath (for cygwin);
2007-12-15, by wenzelm
ExitThread: sleep(300) before delivering EXIT message;
2007-12-15, by wenzelm
reorganized demo;
2007-12-15, by wenzelm
reorganized demo;
2007-12-15, by wenzelm
class Result: replaced FAILURE by SYSTEM (internal notification);
2007-12-15, by wenzelm
non-ML session: run with 'nice', to prevent isabelle process from flooding interactive front-ends (ProofGeneral/XEmacs etc.)
2007-12-15, by wenzelm
recover: not skip over "`";
2007-12-15, by wenzelm
package isabelle;
2007-12-15, by wenzelm
text_of: made even more robust against recurrent errors;
2007-12-15, by wenzelm
added separate_chars;
2007-12-15, by wenzelm
removed unused escape_malformed;
2007-12-15, by wenzelm
outputWrapped: more robust initial synchronization;
2007-12-15, by wenzelm
Result: added STDOUT, SIGNAL;
2007-12-15, by wenzelm
option -m: avoid additional quoting;
2007-12-15, by wenzelm
tuned whitespace;
2007-12-15, by wenzelm
proper termination of stdout thread;
2007-12-15, by wenzelm
added exit thread;
2007-12-14, by wenzelm
tuned diagnostics;
2007-12-14, by wenzelm
run Isabelle process with plain tty interaction;
2007-12-14, by wenzelm
added output protocol specification;
2007-12-14, by wenzelm
tuned;
2007-12-14, by wenzelm
added isatool tty;
2007-12-14, by wenzelm
added ISABELLE_LINE_EDITOR setting;
2007-12-14, by wenzelm
added ISABELLE_LINE_EDITOR;
2007-12-14, by wenzelm
* isatool tty runs Isabelle process with plain tty interaction;
2007-12-14, by wenzelm
nested commands: avoid nested errors;
2007-12-14, by wenzelm
added close_witness;
2007-12-14, by wenzelm
removed syntax in locale left_commutative
2007-12-13, by kleing
changed order in class parameters
2007-12-13, by haftmann
heutistics for type annotations in Haskell
2007-12-13, by haftmann
simplified
2007-12-13, by haftmann
memorizing and exporting destruction rules
2007-12-13, by haftmann
improved rule calculation
2007-12-13, by haftmann
exported axiomsN
2007-12-13, by haftmann
added div/mod examples
2007-12-13, by haftmann
target language div and mod
2007-12-13, by haftmann
clarified heading
2007-12-13, by haftmann
dropped ws
2007-12-13, by haftmann
added lemma
2007-12-13, by haftmann
isatool codegen now returns exit value
2007-12-13, by haftmann
a fold operation for multisets + more lemmas
2007-12-13, by kleing
tuned
2007-12-12, by haftmann
adjusted
2007-12-12, by haftmann
pretty for instantiation and overloading
2007-12-11, by haftmann
continued
2007-12-11, by haftmann
error handling for pathological cases
2007-12-11, by haftmann
dropped induction rule
2007-12-11, by haftmann
dropped Class.prep_spec
2007-12-11, by haftmann
moved lemma odd_pos to theory Parity
2007-12-11, by haftmann
joined StarClasses theory with StarDef
2007-12-11, by haftmann
joined EvenOdd theory with Parity
2007-12-11, by haftmann
tuned
2007-12-11, by haftmann
added simple primitive note
2007-12-10, by haftmann
moved instance parameter management from class.ML to axclass.ML
2007-12-10, by haftmann
tuned header
2007-12-10, by haftmann
switched import from Main to List
2007-12-10, by haftmann
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
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip