isabelle: Graph

merged
2010-05-21, by wenzelm
adjusted to changes in Mapping.thy
2010-05-21, by haftmann
merged
2010-05-21, by haftmann
tuned
2010-05-21, by haftmann
more lemmas about mappings, in particular keys
2010-05-21, by haftmann
refined
2010-05-21, by haftmann
nats in Haskell are readable
2010-05-21, by haftmann
Let rsp and prs in fun_rel/fun_map format
2010-05-21, by Cezary Kaliszyk
tuned zoom_box;
2010-05-21, by wenzelm
print calculation result in the context where the fact is actually defined -- proper externing;
2010-05-21, by wenzelm
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
2010-05-21, by wenzelm
some message styling;
2010-05-21, by wenzelm
simplified message markup, using plain XML.Elem directly;
2010-05-21, by wenzelm
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
2010-05-21, by wenzelm
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
2010-05-21, by wenzelm
bad_result: report fully explicit message;
2010-05-21, by wenzelm
observe additional isabelle-jedit.css for component and user;
2010-05-21, by wenzelm
added checkboxes for debug/tracing filter;
2010-05-21, by wenzelm
more abstract view on prover output messages;
2010-05-21, by wenzelm
added some tooltips;
2010-05-21, by wenzelm
HTML_Panel.handler as overridable method;
2010-05-21, by wenzelm
added Library.undefined (in Scala);
2010-05-21, by wenzelm
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
2010-05-21, by wenzelm
component resize: full handle_resize;
2010-05-21, by wenzelm
speed up some proofs and fix some warnings
2010-05-20, by huffman
merged
2010-05-20, by wenzelm
merged
2010-05-20, by haftmann
proper code generator for complement
2010-05-20, by haftmann
proper document text
2010-05-20, by haftmann
implement Mapping.map_entry
2010-05-20, by haftmann
operations default, map_entry, map_default; more lemmas
2010-05-20, by haftmann
added More_List.thy explicitly
2010-05-20, by haftmann
renamed List_Set to the now more appropriate More_Set
2010-05-20, by haftmann
added theory More_List
2010-05-20, by haftmann
moved generic List operations to theory More_List
2010-05-20, by haftmann
adjusted
2010-05-20, by haftmann
turned old-style mem into an input abbreviation
2010-05-20, by haftmann
zoom font size;
2010-05-20, by wenzelm
added somewhat generic zoom box;
2010-05-20, by wenzelm
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
2010-05-20, by wenzelm
mutate displayed document synchronously in Swing thread, for improved robustness;
2010-05-20, by wenzelm
read style sheets only once;
2010-05-20, by wenzelm
handle component resize for output / HTML panel;
2010-05-20, by wenzelm
Isabelle_System: allow explicit isabelle_home argument;
2010-05-20, by wenzelm
enable shell script editor mode;
2010-05-20, by wenzelm
merged
2010-05-20, by wenzelm
merged
2010-05-20, by bulwahn
deactivated timing of infering modes
2010-05-20, by bulwahn
adapting examples
2010-05-19, by bulwahn
changing operations for accessing data to work with contexts
2010-05-19, by bulwahn
removed unnecessary Thm.transfer in the predicate compiler
2010-05-19, by bulwahn
changing compilation to work only with contexts; adapting quickcheck
2010-05-19, by bulwahn
removing unused argument in print_modes function
2010-05-19, by bulwahn
moving towards working with proof contexts in the predicate compiler
2010-05-19, by bulwahn
improved values command to handle a special case with tuples and polymorphic predicates more correctly
2010-05-19, by bulwahn
improved behaviour of defined_functions in the predicate compiler
2010-05-19, by bulwahn
move some example files into new HOLCF/Tutorial directory
2010-05-19, by huffman
remove redundant hdvd relation
2010-05-19, by huffman
remove unnecessary constant Fixrec.bind
2010-05-19, by huffman
add section about fixrec definitions with looping simp rules
2010-05-19, by huffman
more informative error message for fixrec when continuity proof fails
2010-05-19, by huffman
determine margin just before rendering -- proper reformatting when updating;
2010-05-20, by wenzelm
simplified alignment via FlowPanel;
2010-05-20, by wenzelm
more systematic treatment of physical document wrt. font size etc.;
2010-05-20, by wenzelm
tuned;
2010-05-20, by wenzelm
general Isabelle_System.try_read;
2010-05-20, by wenzelm
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-20, by wenzelm
inverted "Freeze" to "Follow", which is the default;
2010-05-20, by wenzelm
basic controls to freeze/update prover results;
2010-05-19, by wenzelm
show fully detailed protocol messages;
2010-05-19, by wenzelm
some updates following src/Tools/jEdit/dist-template/settings;
2010-05-19, by wenzelm
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
2010-05-19, by haftmann
merged
2010-05-19, by haftmann
dropped legacy_unconstrainT
2010-05-19, by haftmann
new version of triv_of_class machinery without legacy_unconstrain
2010-05-19, by haftmann
merge
2010-05-19, by haftmann
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
2010-05-19, by haftmann
remove several redundant lemmas about floor and ceiling
2010-05-18, by huffman
merged
2010-05-18, by huffman
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-17, by huffman
simplify proof
2010-05-17, by huffman
simplify proof
2010-05-17, by huffman
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
2010-05-17, by huffman
prefer structure Keyword and Parse;
2010-05-18, by wenzelm
merged
2010-05-18, by wenzelm
merged
2010-05-17, by huffman
remove simp attribute from square_eq_1_iff
2010-05-17, by huffman
merged
2010-05-17, by blanchet
make sure chained facts don't pop up in the metis proof
2010-05-17, by blanchet
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-17, by blanchet
generate proper arity declarations for TFrees for SPASS's DFG format;
2010-05-17, by blanchet
identify common SPASS error more clearly
2010-05-17, by blanchet
remove simp attribute from power2_eq_1_iff
2010-05-17, by huffman
dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-17, by haftmann
dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-17, by haftmann
do not open Legacy by default;
2010-05-18, by wenzelm
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-17, by wenzelm
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-17, by wenzelm
tuned;
2010-05-17, by wenzelm
tuned signature;
2010-05-17, by wenzelm
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
2010-05-17, by wenzelm
centralized legacy aliases;
2010-05-17, by wenzelm
prefer structure Parse_Spec;
2010-05-16, by wenzelm
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15, by wenzelm
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15, by wenzelm
renamed structure ValueParse to Parse_Value;
2010-05-15, by wenzelm
refer directly to structure Keyword and Parse;
2010-05-15, by wenzelm
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
2010-05-15, by wenzelm
renamed Outer_Parse to Parse (in Scala);
2010-05-15, by wenzelm
renamed Outer_Keyword to Keyword (in Scala);
2010-05-15, by wenzelm
avoid open Conv;
2010-05-15, by wenzelm
less pervasive names from structure Thm;
2010-05-15, by wenzelm
less pervasive names from structure Thm;
2010-05-15, by wenzelm
tuned;
2010-05-15, by wenzelm
merged
2010-05-15, by wenzelm
add real_le_linear to list of legacy theorem names
2010-05-15, by huffman
make SML/NJ happy
2010-05-15, by blanchet
removed unused conversions;
2010-05-15, by wenzelm
tuned header;
2010-05-15, by wenzelm
moved normarith.ML where it is actually used;
2010-05-15, by wenzelm