isabelle: Graph

less complex organization of cooper source code
2010-05-10, by haftmann
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
2010-05-10, by haftmann
add real_mult_commute to legacy theorem names
2010-05-10, by huffman
new construction of real numbers using Cauchy sequences
2010-05-10, by huffman
add more credits to ex/Dedekind_Real.thy
2010-05-10, by huffman
put construction of reals using Dedekind cuts in HOL/ex
2010-05-10, by huffman
disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
2010-05-11, by wenzelm
simple dialogs: ensure Swing thread;
2010-05-10, by wenzelm
font size re-adjustment according to Lobo internals;
2010-05-10, by wenzelm
Scala for Netbeans 6.8v1.1.0rc2;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-05-10, by wenzelm
more convenient look-and-feel setup;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;
2010-05-10, by wenzelm
updated to jedit 4.3.2;
2010-05-10, by wenzelm
ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
2010-05-10, by wenzelm
adapted to scala-2.8.0.RC2;
2010-05-10, by wenzelm
merged
2010-05-10, by wenzelm
real_mult_commute -> mult_commute
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
remove a couple of redundant lemmas; simplify some proofs
2010-05-09, by huffman
merged
2010-05-09, by huffman
add lemmas one_less_inverse and one_le_inverse
2010-05-08, by huffman
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
2010-05-09, by krauss
added lemmas rel_comp_UNION_distrib(2)
2010-05-09, by krauss
made SML/NJ happy;
2010-05-08, by wenzelm
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09, by wenzelm
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09, by wenzelm
just one version of Thm.unconstrainT, which affects all variables;
2010-05-09, by wenzelm
added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
2010-05-09, by wenzelm
tuned;
2010-05-09, by wenzelm
removed unused "option" variants of "same" operations;
2010-05-09, by wenzelm
more basic replacement of newlines;
2010-05-09, by wenzelm
static Symbol.spaces;
2010-05-09, by wenzelm
proper use of var stopped;
2010-05-08, by wenzelm
removed junk;
2010-05-08, by wenzelm
tuned headers;
2010-05-08, by wenzelm
tuned;
2010-05-08, by wenzelm
merged
2010-05-08, by wenzelm
merged
2010-05-08, by haftmann
moved normalization proof tool infrastructure to canonical algebraic classes
2010-05-08, by haftmann
added lemmas
2010-05-08, by nipkow
merged
2010-05-08, by haftmann
renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07, by haftmann
delete Groebner_Basis directory -- only one file left
2010-05-07, by haftmann
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-07, by haftmann
merged
2010-05-07, by haftmann
moved lemma zdvd_period to theory Int
2010-05-07, by haftmann
tuned;
2010-05-08, by wenzelm
discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08, by wenzelm
tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08, by wenzelm
unified/simplified Pretty.margin_default;
2010-05-08, by wenzelm
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-08, by wenzelm
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
2010-05-08, by wenzelm
tuned signature;
2010-05-08, by wenzelm
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08, by wenzelm
back-patching of axclass proofs;
2010-05-08, by wenzelm
back-patching via Single_Assignment.var;
2010-05-08, by wenzelm
support several sidekick parsers -- very basic default parser;
2010-05-07, by wenzelm
sidekick: unformatted content, notably without newlines;
2010-05-07, by wenzelm
unformatted output;
2010-05-07, by wenzelm
output symbolic pretty printing markup and format in the front end;
2010-05-07, by wenzelm
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
2010-05-07, by wenzelm
tuned;
2010-05-07, by wenzelm
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-07, by wenzelm
use existing undefined function;
2010-05-07, by wenzelm
merged
2010-05-07, by wenzelm
removed semicolons
2010-05-07, by krauss
rule subrelI (for nice Isar proofs of relation inequalities)
2010-05-07, by krauss
merged
2010-05-07, by wenzelm
merged
2010-05-07, by haftmann
prefix normalizing replaces class_semiring
2010-05-07, by haftmann
xsymbolized
2010-05-06, by haftmann
moved method syntax here
2010-05-06, by haftmann
tuned proof
2010-05-06, by haftmann
former free-floating field_comp_conv now in structure Normalizer
2010-05-06, by haftmann
proper sublocales; no free-floating ML sections
2010-05-06, by haftmann
moved some lemmas from Groebner_Basis here
2010-05-06, by haftmann
revert to loose merge semantics
2010-05-06, by haftmann
merged
2010-05-06, by haftmann
moved generic lemmas to appropriate places
2010-05-06, by haftmann
tuned
2010-05-06, by haftmann
dropped duplicate comp_arith
2010-05-06, by haftmann
avoid open; tuned references to theorems
2010-05-06, by haftmann
avoid references to groebner bases in names which have no references to groebner bases
2010-05-06, by haftmann
tuned whitespace
2010-05-06, by haftmann
tuned headings
2010-05-06, by haftmann
avoid open
2010-05-06, by haftmann
tuned internal structure
2010-05-06, by haftmann
fail on merge of conflicting normalization entries: functions are not mergable
2010-05-06, by haftmann
more canonical data administration
2010-05-06, by haftmann
removed former algebra presimpset entirely
2010-05-06, by haftmann
removed former algebra presimpset from accessor
2010-05-06, by haftmann
removed former algebra presimpset from signature
2010-05-06, by haftmann
moved presimplification rules for algebraic methods into named thms functor
2010-05-06, by haftmann
tuned whitespace; dropped superfluous open
2010-05-06, by haftmann
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-05-06, by haftmann
moved nat_arith ot Nat_Numeral: clarified normalizer setup
2010-05-05, by haftmann
dropped unused file
2010-05-05, by haftmann
dropped Id
2010-05-05, by haftmann
remove unused constant preal_of_rat; remove several unused lemmas about preals
2010-05-06, by huffman
respectfullness and preservation of prod_rel
2010-05-06, by Cezary Kaliszyk
ProofContext.init_global
2010-05-06, by haftmann
merged
2010-05-06, by haftmann
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-05, by haftmann
constant name access lattice is not in use any longer
2010-05-06, by haftmann
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
2010-05-06, by wenzelm
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06, by wenzelm
added separate;
2010-05-06, by wenzelm
basic formatting of pretty trees;
2010-05-06, by wenzelm
added content_length;
2010-05-06, by wenzelm
slightly more general Library.chunks;
2010-05-06, by wenzelm
misc tuning -- accumulate body via ListBuffer;
2010-05-06, by wenzelm
basic support for symbolic pretty printing;
2010-05-06, by wenzelm
extractors for document updates;
2010-05-06, by wenzelm
extractors for outer keyword declarations;
2010-05-06, by wenzelm
eliminated deprecated "--" method;
2010-05-05, by wenzelm
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
2010-05-05, by wenzelm