isabelle: Graph

more user aliases;
2011-09-24, by wenzelm
fixed IsaMakefile action for HOL-TPTP.
2011-09-24, by sultana
prefer socket comminication on Cygwin, which is more stable here than fifos;
2011-09-23, by wenzelm
tuned proof;
2011-09-23, by wenzelm
made SML/NJ happy;
2011-09-23, by wenzelm
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
2011-09-23, by wenzelm
updated header;
2011-09-23, by wenzelm
merged;
2011-09-23, by wenzelm
reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
2011-09-23, by blanchet
first step towards extending Minipick with more translations
2011-09-23, by blanchet
Include keywords print_coercions and print_coercion_maps
2011-09-23, by berghofe
local coercion insertion algorithm to support complex coercions
2011-08-17, by traytel
printing and deleting of coercions
2011-08-17, by traytel
raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
2011-09-23, by wenzelm
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
2011-09-23, by wenzelm
augment existing print mode;
2011-09-23, by wenzelm
explicit option for socket vs. fifo communication;
2011-09-23, by wenzelm
tuned proof;
2011-09-23, by wenzelm
synchronized section names with manual
2011-09-23, by blanchet
merged;
2011-09-23, by wenzelm
discontinued legacy theorem names from RealDef.thy
2011-09-22, by huffman
merged
2011-09-22, by huffman
discontinued HOLCF legacy theorem names
2011-09-22, by huffman
take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
2011-09-22, by blanchet
Moved extraction part of Higman's lemma to separate theory to allow reuse in
2011-09-22, by berghofe
Removed hcentering and vcentering options, since they are not supported
2011-09-22, by berghofe
merged
2011-09-22, by berghofe
Added documentation for HOL-SPARK
2011-09-22, by berghofe
drop partial monomorphic instances in Metis, like in Sledgehammer
2011-09-22, by blanchet
better type reconstruction -- prevents ill-instantiations in proof replay
2011-09-22, by blanchet
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
2011-09-22, by hoelzl
changing quickcheck_timeout to 30 seconds in mutabelle's testing
2011-09-22, by bulwahn
adding post-processing of terms to narrowing-based Quickcheck
2011-09-22, by bulwahn
HOL/ex/ROOT.ML: only list BinEx once
2011-09-21, by huffman
merged
2011-09-21, by huffman
remove redundant instantiation ereal :: power
2011-09-21, by huffman
reintroduced Minipick as Nitpick example
2011-09-21, by blanchet
tuned comment
2011-09-21, by blanchet
merged
2011-09-21, by huffman
Extended_Real_Limits: generalize some lemmas
2011-09-20, by huffman
add lemmas within_empty and tendsto_bot;
2011-09-20, by huffman
made SML/NJ happy;
2011-09-22, by wenzelm
abstract System_Channel in ML (cf. Scala version);
2011-09-22, by wenzelm
alternative Socket_Channel;
2011-09-21, by wenzelm
more abstract wrapping of fifos as System_Channel;
2011-09-21, by wenzelm
slightly more general Socket_IO as part of Pure;
2011-09-21, by wenzelm
more hints on Z3 configuration;
2011-09-21, by wenzelm
reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);
2011-09-21, by wenzelm
renamed inv -> filter
2011-09-21, by nipkow
Added proofs about narowing
2011-09-21, by nipkow
added missing makefile dependence
2011-09-21, by nipkow
added example
2011-09-21, by nipkow
tuned
2011-09-21, by nipkow
refined comment
2011-09-21, by nipkow
fixed two typos in IMP (by Jean Pichon)
2011-09-21, by kleing
merged
2011-09-21, by nipkow
Updated IMP to use new induction method
2011-09-20, by nipkow
New proof method "induction" that gives induction hypotheses the name IH.
2011-09-20, by nipkow
official status for UN_singleton
2011-09-20, by haftmann
tuned specification and lemma distribution among theories; tuned proofs
2011-09-20, by haftmann
more careful treatment of initial update, similar to output panel;
2011-09-20, by wenzelm
proper fact binding;
2011-09-20, by wenzelm
syntactic improvements and tuning names in the code generator due to Florian's code review
2011-09-20, by bulwahn
match types when applying mono_thm -- previous export generalizes type variables;
2011-09-20, by krauss
fixed headers;
2011-09-19, by wenzelm
less ambiguous syntax;
2011-09-19, by wenzelm
tuned proofs;
2011-09-19, by wenzelm
merged
2011-09-19, by wenzelm
catch PatternMatchFail exceptions in narrowing-based quickcheck
2011-09-19, by bulwahn
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
2011-09-19, by bulwahn
ensuring that some constants are generated in the source code by adding calls in ensure_testable
2011-09-19, by bulwahn
adding abstraction layer; more precise function names
2011-09-19, by bulwahn
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
2011-09-19, by bulwahn
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
2011-09-19, by bulwahn
only annotating constants with sort constraints
2011-09-19, by bulwahn
also adding type annotations for the dynamic invocation
2011-09-19, by bulwahn
removed legacy lemmas in Complete_Lattices
2011-09-19, by noschinl
increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling
2011-09-19, by bulwahn
more isatest stats;
2011-09-19, by wenzelm
refined Symbol.is_symbolic -- cover recoded versions as well;
2011-09-19, by wenzelm
double clicks switch to document node buffer;
2011-09-19, by wenzelm
tuned;
2011-09-19, by wenzelm
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
2011-09-19, by wenzelm
at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
2011-09-19, by wenzelm
instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);
2011-09-19, by wenzelm
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
2011-09-19, by wenzelm
imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;
2011-09-19, by wenzelm
merged
2011-09-18, by huffman
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
2011-09-15, by huffman
removed obsolete patches for PG 4.1;
2011-09-18, by wenzelm
additional space for borderless UI;
2011-09-18, by wenzelm
more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);
2011-09-18, by wenzelm
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
2011-09-18, by wenzelm
isatest settings for macbroy6 (Mac OS X Lion);
2011-09-18, by wenzelm
more Mac OS reference hardware;
2011-09-18, by wenzelm
updated to SML/NJ 110.73;
2011-09-18, by wenzelm
tentative announcement based on current NEWS;
2011-09-18, by wenzelm
tuned;
2011-09-18, by wenzelm
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
2011-09-18, by wenzelm
updated for release;
2011-09-18, by wenzelm
tuned;
2011-09-18, by wenzelm
updated generated file;
2011-09-18, by wenzelm
updated Complete_Lattices;
2011-09-18, by wenzelm
some tuning and re-ordering for release;
2011-09-18, by wenzelm
misc tuning for release;
2011-09-18, by wenzelm
more contributors;
2011-09-18, by wenzelm
tuned proofs;
2011-09-18, by wenzelm
tweak keyboard shortcuts for Mac OS X;
2011-09-18, by wenzelm
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
2011-09-18, by wenzelm
finite sequences as useful as introductory example;
2011-09-18, by wenzelm
discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;
2011-09-18, by wenzelm
graph traversal in topological order;
2011-09-18, by wenzelm
Document.Node.Name convenience;
2011-09-17, by wenzelm
more precise painting;
2011-09-17, by wenzelm
more elaborate Node_Renderer, which paints node_name.theory only;
2011-09-17, by wenzelm
raised default log level -- to avoid confusing warning about scala.tools.nsc.plugins.Plugin, which is mistaken as jEdit plugin;
2011-09-17, by wenzelm
tuned signature;
2011-09-17, by wenzelm
more careful traversal of theory dependencies to retain standard import order;
2011-09-17, by wenzelm
sane default for class Thy_Load;
2011-09-17, by wenzelm
removed obsolete patches for PG 4.1;
2011-09-17, by wenzelm
specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;
2011-09-17, by wenzelm
added "isabelle scalac" convenience;
2011-09-17, by wenzelm
Symbol.explode as in ML;
2011-09-17, by wenzelm
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
2011-09-17, by wenzelm
dropped unused argument – avoids problem with SML/NJ
2011-09-17, by haftmann
tuned spacing
2011-09-17, by haftmann
tuned
2011-09-17, by haftmann
tuned post fixpoint setup
2011-09-17, by nipkow
merged
2011-09-17, by nipkow
when applying induction rules, remove names of assumptions that come
2011-09-16, by nipkow
remove stray "using [[simp_trace]]"
2011-09-16, by noschinl
tune indenting
2011-09-16, by noschinl
removed unused legacy lemma names, some comment cleanup.
2011-09-16, by kleing
removed word_neq_0_conv from simpset, it's almost never wanted.
2011-09-16, by kleing
removed further legacy rules from Complete_Lattices
2011-09-15, by hoelzl
NEWS on Complete_Lattices, Lattices
2011-09-15, by noschinl
tail recursive proof preprocessing (needed for huge proofs)
2011-09-15, by blanchet
tuning
2011-09-15, by blanchet
merged
2011-09-15, by nipkow
revised AbsInt and added widening and narrowing
2011-09-15, by nipkow
updated comment
2011-09-14, by haftmann
updated generated code
2011-09-14, by haftmann
tuned
2011-09-13, by haftmann
renamed Complete_Lattices lemmas, removed legacy names
2011-09-14, by hoelzl
merged
2011-09-14, by noschinl
create central list for language extensions used by the haskell code generator
2011-09-14, by noschinl
observe distinction between sets and predicates
2011-09-14, by boehmes
merged
2011-09-14, by nipkow
cleand up AbsInt fixpoint iteration; tuned syntax
2011-09-14, by nipkow
tuned proofs
2011-09-13, by huffman
tuned proofs
2011-09-13, by huffman
remove some redundant [simp] declarations;
2011-09-13, by huffman
tune proofs
2011-09-13, by noschinl
tune simpset for Complete_Lattices
2011-09-13, by noschinl
merged
2011-09-13, by bulwahn
added lemma motivated by a more specific lemma in the AFP-KBPs theories
2011-09-13, by bulwahn
simplified unsound proof detection by removing impossible case
2011-09-13, by blanchet
correcting NEWS
2011-09-13, by bulwahn
correcting theory name and dependencies
2011-09-13, by bulwahn
renamed AList_Impl to AList
2011-09-13, by bulwahn
fastsimp -> fastforce in doc
2011-09-13, by nipkow
fix typo
2011-09-12, by huffman
shorten proof of frontier_straddle
2011-09-12, by huffman
NEWS and CONTRIBUTORS
2011-09-12, by huffman
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12, by huffman
simplify proofs using LIMSEQ lemmas
2011-09-12, by huffman
remove trivial lemma Lim_at_iff_LIM
2011-09-12, by huffman
fix typos
2011-09-12, by huffman
NEWS for euclidean_space class
2011-09-12, by huffman
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
2011-09-12, by huffman
adding NEWS and CONTRIBUTORS
2011-09-12, by hoelzl
merged
2011-09-12, by bulwahn
correcting imports after splitting and renaming AssocList
2011-09-12, by bulwahn
tuned
2011-09-12, by bulwahn
moving connection of association lists to Mappings into a separate theory
2011-09-12, by bulwahn
adding NEWS and CONTRIBUTORS
2011-09-12, by bulwahn
tuned some symbol that probably went there by some strange encoding issue
2011-09-12, by bulwahn
added my contributions to NEWS and CONTRIBUTORS
2011-09-12, by blanchet
fixed type intersection (again)
2011-09-12, by blanchet
consistent option naming
2011-09-12, by blanchet
NEWS fastsimp -> fastforce
2011-09-12, by nipkow
new fastforce replacing fastsimp - less confusing name
2011-09-12, by nipkow
merged
2011-09-11, by wenzelm
NEWS for Library/Product_Lattice.thy
2011-09-11, by huffman
misc tuning and clarification;
2011-09-11, by wenzelm
merged
2011-09-11, by wenzelm
merged
2011-09-11, by huffman
tuned proofs
2011-09-11, by huffman
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
2011-09-11, by huffman
more CONTRIBUTORS;
2011-09-11, by wenzelm
persistent ISABELLE_INTERFACE_CHOICE;
2011-09-11, by wenzelm
explicit choice of interface;
2011-09-11, by wenzelm
more orthogonal signature;
2011-09-11, by wenzelm
updates for release;
2011-09-11, by wenzelm
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
2011-09-11, by wenzelm
some updates of PLATFORMS;
2011-09-11, by wenzelm
more README;
2011-09-11, by wenzelm
merged
2011-09-10, by wenzelm
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
2011-09-10, by krauss
misc tuning;
2011-09-10, by wenzelm
misc tuning and clarification;
2011-09-10, by wenzelm
speed up slow proof;
2011-09-10, by wenzelm
merged
2011-09-10, by wenzelm
more modularization
2011-09-10, by haftmann
stronger colors (as background);
2011-09-10, by wenzelm
some color scheme for theory status;
2011-09-10, by wenzelm
some keyboard shortcuts for important actions;
2011-09-10, by wenzelm
explicit jEdit actions -- to enable key mappings, for example;
2011-09-10, by wenzelm
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
2011-09-10, by wenzelm
tuned usage;
2011-09-10, by wenzelm
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
2011-09-10, by wenzelm
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-09-10, by haftmann
fixed definition of type intersection (soundness bug)
2011-09-10, by blanchet
continue with minimization in debug mode in spite of unsoundness
2011-09-10, by blanchet
generalize lemma of_nat_number_of_eq to class number_semiring
2011-09-09, by huffman
merged
2011-09-09, by bulwahn
stating more explicitly our expectation that these two terms have the same term structure
2011-09-09, by bulwahn
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
2011-09-09, by bulwahn
made SML/NJ happy
2011-09-09, by blanchet
call ghc with -XEmptyDataDecls
2011-09-08, by noschinl
merged
2011-09-09, by nipkow
tuned headers
2011-09-09, by nipkow
Library/Saturated.thy: number_semiring class instance
2011-09-08, by huffman
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-09-08, by huffman
merged
2011-09-08, by huffman
remove unnecessary intermediate lemmas
2011-09-08, by huffman
added syntactic classes for "inf" and "sup"
2011-09-09, by krauss
prove existence, uniqueness, and other properties of complex arg function
2011-09-08, by huffman
tuned
2011-09-08, by huffman
remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-08, by huffman
tuned
2011-09-08, by huffman
merged
2011-09-08, by haftmann
tuned
2011-09-08, by haftmann
merged
2011-09-08, by haftmann
merged
2011-09-07, by haftmann
merged
2011-09-06, by haftmann
merged
2011-09-06, by haftmann
merged
2011-09-06, by haftmann
tuned
2011-09-05, by haftmann
merged
2011-09-05, by haftmann
tuned
2011-09-05, by haftmann
tuned
2011-09-04, by haftmann
fixed computation of "in_conj" for polymorphic encodings
2011-09-08, by blanchet
add some new lemmas about cis and rcis;
2011-09-07, by huffman
Complex.thy: move theorems into appropriate subsections
2011-09-07, by huffman
merged
2011-09-07, by huffman
remove redundant lemma complex_of_real_minus_one
2011-09-07, by huffman
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-07, by huffman
removed unused lemma sin_cos_squared_add2_mult
2011-09-07, by huffman
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-07, by huffman
avoid using legacy theorem names
2011-09-07, by huffman
merged
2011-09-08, by wenzelm
theory of saturated naturals contributed by Peter Gammie
2011-09-07, by haftmann
theory of saturated naturals contributed by Peter Gammie
2011-09-07, by haftmann
lemmas about +, *, min, max on nat
2011-09-07, by haftmann
update Sledgehammer docs
2011-09-07, by blanchet
added new tagged encodings to Metis tests
2011-09-07, by blanchet
also implemented ghost version of the tagged encodings
2011-09-07, by blanchet
added new guards encoding to test
2011-09-07, by blanchet
smarter explicit apply business
2011-09-07, by blanchet
started work on ghost type arg encoding
2011-09-07, by blanchet
stricted type encoding parsing
2011-09-07, by blanchet
more substructural sharing to gain significant compression;
2011-09-08, by wenzelm
XML.cache for partial sharing (strings only);
2011-09-07, by wenzelm
platform-specific look and feel;
2011-09-07, by wenzelm
more README;
2011-09-07, by wenzelm
clarified terminology;
2011-09-07, by wenzelm
no print_state for final proof commands, which return to theory state;
2011-09-07, by wenzelm
NEWS on IsabelleText font;
2011-09-07, by wenzelm
explicit join_syntax ensures command transaction integrity of 'theory';
2011-09-07, by wenzelm
some updates for release;
2011-09-07, by wenzelm
some tuning for release;
2011-09-07, by wenzelm
updated file locations;
2011-09-07, by wenzelm
merged
2011-09-07, by wenzelm
merged
2011-09-07, by bulwahn
removing previously used function locally_monomorphic in the code generator
2011-09-07, by bulwahn
setting const_sorts to false in the type inference of the code generator
2011-09-07, by bulwahn
adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
2011-09-07, by bulwahn
removing previous crude approximation to add type annotations to disambiguate types
2011-09-07, by bulwahn
adding minimalistic implementation for printing the type annotations
2011-09-07, by bulwahn
adding call to disambiguation annotations
2011-09-07, by bulwahn
adding type inference for disambiguation annotations in code equation
2011-09-07, by bulwahn
adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07, by bulwahn
changing const type to pass along if typing annotations are necessary for disambigous terms
2011-09-07, by bulwahn
fixed THF type constructor syntax
2011-09-07, by blanchet
tweaking polymorphic TFF and THF output
2011-09-07, by blanchet
parse new experimental '@' encodings
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
clarified import;
2011-09-07, by wenzelm
tuned/simplified proofs;
2011-09-07, by wenzelm
tuned proofs;
2011-09-07, by wenzelm
deactivate unfinished charset provider for now, to avoid user confusion;
2011-09-07, by wenzelm
more NEWS;
2011-09-07, by wenzelm
added "check" button: adhoc change to full buffer perspective;
2011-09-07, by wenzelm
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
2011-09-07, by wenzelm
separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
2011-09-07, by blanchet
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
make mangling sound w.r.t. type arguments
2011-09-07, by blanchet
make "filter_type_args" more robust if the actual arity is higher than the declared one
2011-09-07, by blanchet
updated Sledgehammer documentation
2011-09-07, by blanchet
rationalize uniform encodings
2011-09-07, by blanchet
merged
2011-09-06, by huffman
avoid using legacy theorem names
2011-09-06, by huffman
merged
2011-09-06, by huffman
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-06, by huffman
HOL/Import: Update HOL4 generated files to current Isabelle.
2011-09-07, by Cezary Kaliszyk
tuned proofs;
2011-09-07, by wenzelm
remove some unnecessary simp rules from simpset
2011-09-06, by huffman
some Isabelle/jEdit NEWS;
2011-09-06, by wenzelm
more README;
2011-09-06, by wenzelm
merged
2011-09-06, by wenzelm
merged
2011-09-06, by huffman
simplify proof of tan_half, removing unused assumptions
2011-09-06, by huffman
convert some proofs to Isar-style
2011-09-06, by huffman
added dummy polymorphic THF system
2011-09-06, by blanchet
added some examples for pattern and weight annotations
2011-09-06, by boehmes
merged
2011-09-06, by bulwahn
avoid "Code" as structure name (cf. 3bc39cfe27fe)
2011-09-06, by bulwahn
remove duplicate copy of lemma sqrt_add_le_add_sqrt
2011-09-06, by huffman
remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06, by huffman
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-06, by huffman
merged
2011-09-06, by huffman
add lemmas about arctan;
2011-09-05, by huffman
convert lemma cos_total to Isar-style proof
2011-09-05, by huffman
added new lemmas
2011-09-06, by nipkow
updated Sledgehammer's docs
2011-09-06, by blanchet
cleanup "simple" type encodings
2011-09-06, by blanchet
merge
2011-09-06, by Cezary Kaliszyk
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
2011-09-06, by Cezary Kaliszyk
tuning
2011-09-06, by blanchet
drop more type arguments soundly, when they can be deduced from the arg types
2011-09-06, by blanchet
bulk reports for improved message throughput;
2011-09-06, by wenzelm
bulk reports for improved message throughput;
2011-09-06, by wenzelm
tuned signature;
2011-09-06, by wenzelm
more specific message channels to avoid potential bottle-neck of raw_messages;
2011-09-06, by wenzelm
buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
2011-09-06, by wenzelm
more abstract receiver interface;
2011-09-06, by wenzelm
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
2011-09-06, by wenzelm
convert lemma cos_is_zero to Isar-style
2011-09-05, by huffman
merged
2011-09-05, by huffman
convert lemma sin_gt_zero to Isar style;
2011-09-05, by huffman
modify lemma sums_group, and shorten proofs that use it
2011-09-05, by huffman
generalize some lemmas
2011-09-05, by huffman
add lemmas cos_arctan and sin_arctan
2011-09-05, by huffman
tuned indentation
2011-09-05, by huffman
more visible outdated_color;
2011-09-05, by wenzelm
commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
2011-09-05, by wenzelm
tuned imports;
2011-09-05, by wenzelm
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
2011-09-05, by blanchet
tuned
2011-09-05, by boehmes
tuned
2011-09-05, by boehmes
filter out all schematic theorems if the problem contains no ground constants
2011-09-05, by boehmes
merged
2011-09-04, by huffman
tuned comments
2011-09-04, by huffman
simplify proof of Bseq_mono_convergent
2011-09-04, by huffman
merged
2011-09-04, by wenzelm
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
2011-09-04, by huffman
remove redundant lemmas expi_add and expi_zero
2011-09-04, by huffman
remove redundant lemmas about LIMSEQ
2011-09-04, by huffman
introduce abbreviation 'int' earlier in Int.thy
2011-09-04, by huffman
remove unused assumptions from natceiling lemmas
2011-09-04, by huffman
move lemmas nat_le_iff and nat_mono into Int.thy
2011-09-04, by huffman
eliminated markup for plain identifiers (frequent but insignificant);
2011-09-04, by wenzelm
simplified signatures;
2011-09-04, by wenzelm
synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04, by wenzelm
tuned document;
2011-09-04, by wenzelm
improved handling of extended styles and hard tabs when prover is inactive;
2011-09-04, by wenzelm
mark hard tabs as single chunks, as required by jEdit;
2011-09-04, by wenzelm
updated READMEs;
2011-09-04, by wenzelm
property "tooltip-dismiss-delay" is edited in ms, not seconds;
2011-09-04, by wenzelm
moved XML/YXML to src/Pure/PIDE;
2011-09-04, by wenzelm
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
2011-09-04, by wenzelm
pseudo-definition for perms on sets; tuned
2011-09-04, by haftmann
remove duplicate lemma nat_zero in favor of nat_0
2011-09-03, by huffman
merged
2011-09-03, by huffman
merged
2011-09-03, by huffman
modify nominal packages to better respect set/pred distinction
2011-09-03, by huffman
merged
2011-09-03, by huffman
remove unused assumption from lemma posreal_complete
2011-09-03, by huffman
tuned specifications
2011-09-03, by haftmann
merged
2011-09-03, by haftmann