isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

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