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.
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
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
where/of: do not allow schematic variables here!
2007-11-08, by wenzelm
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
2007-11-08, by wenzelm
discontinued legacy vars;
2007-11-08, by wenzelm
removed unused read_def_terms';
2007-11-08, by wenzelm
eliminated illegal schematic variables in where/of;
2007-11-08, by wenzelm
eliminated illegal schematic variables in where/of;
2007-11-08, by wenzelm
x86_64: fall back on x86 (more efficient);
2007-11-08, by wenzelm
tuned comments;
2007-11-08, by wenzelm
renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-08, by wenzelm
renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-08, by wenzelm
synchronize_syntax: improved declare_const (still inactive);
2007-11-08, by wenzelm
added const_proper;
2007-11-08, by wenzelm
added evaluation
2007-11-08, by nipkow
fix
2007-11-08, by nipkow
new general syntax
2007-11-08, by nipkow
tuned
2007-11-08, by nipkow
updated to notation and abbreviation
2007-11-08, by nipkow
added purify_sym
2007-11-08, by haftmann
tuned
2007-11-08, by haftmann
duv, mod, int conversion
2007-11-08, by haftmann
ProofContext.read_const';
2007-11-07, by wenzelm
Syntax.read_typ;
2007-11-07, by wenzelm
export read_const';
2007-11-07, by wenzelm
Syntax.read_typ;
2007-11-07, by wenzelm
added inductive
2007-11-07, by nipkow
attribute where/of: proper Syntax.parse/check;
2007-11-07, by wenzelm
discontinued ProofContext.read_prop_legacy;
2007-11-07, by wenzelm
discontinued ProofContext.read_prop_legacy;
2007-11-07, by wenzelm
refined Variable.declare_const;
2007-11-07, by wenzelm
refined notion of consts within the local scope;
2007-11-07, by wenzelm
tuned signature;
2007-11-07, by wenzelm
removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-11-07, by wenzelm
map and prefix
2007-11-07, by kleing
activated HOL-SizeChange;
2007-11-06, by wenzelm
tuned;
2007-11-06, by wenzelm
read_const/legacy_intern_skolem: cover consts within the local scope;
2007-11-06, by wenzelm
synchronize_syntax: declare operations within the local scope of fixes/consts
2007-11-06, by wenzelm
fixed spelling;
2007-11-06, by wenzelm
added is_const/declare_const for local scope of fixes/consts;
2007-11-06, by wenzelm
removed dependencies on Size_Change_Termination from HOL-Library;
2007-11-06, by wenzelm
moved stuff about size change termination to its own session
2007-11-06, by krauss
clarifying comment
2007-11-06, by haftmann
clarified merge
2007-11-06, by haftmann
Class.init now similiar to Locale.init
2007-11-06, by haftmann
CRITICAL force
2007-11-06, by haftmann
autoquickcheck message
2007-11-06, by haftmann
added explicit signature
2007-11-06, by haftmann
simplified specification of *_abs class
2007-11-06, by haftmann
tuned;
2007-11-06, by wenzelm
added autoquickcheck
2007-11-06, by haftmann
removed subclass edge ordered_ring < lordered_ring
2007-11-06, by haftmann
renamed lordered_*_* to lordered_*_add_*; further localization
2007-11-06, by haftmann
tuned satisfy_thm;
2007-11-05, by wenzelm
removed unused compose_hhf, comp_hhf;
2007-11-05, by wenzelm
corrected fucked up integer tuning
2007-11-05, by obua
misc lemmas about prefix, postfix, and parallel
2007-11-05, by kleing
add root.bib for Word document
2007-11-05, by kleing
move itself into HOL types
2007-11-05, by kleing
rev_nth
2007-11-05, by kleing
tranclD2 (tranclD at the other end) + trancl_power
2007-11-05, by kleing
acknowledge authors
2007-11-05, by kleing
cite Jeremy's avocs article
2007-11-05, by kleing
simplified LocalTheory.reinit;
2007-11-05, by wenzelm
misc cleanup of init functions;
2007-11-05, by wenzelm
TheoryTarget.context;
2007-11-05, by wenzelm
simplified LocalTheory.reinit;
2007-11-05, by wenzelm
improved error message for missing predicates;
2007-11-05, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip