Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-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.
clarified platform dependency;
2012-10-04, by wenzelm
updated crontab and afp-poly settings
2012-10-04, by Gerwin Klein
thread the right local theory through + reenable parallel proofs for previously problematic theories
2012-10-03, by blanchet
made code more conform to rest of BNF package
2012-10-03, by blanchet
more error positions;
2012-10-03, by wenzelm
more explicit show_type_constraint, show_sort_constraint;
2012-10-03, by wenzelm
recovered print translation after 'a => bool to 'a set change;
2012-10-03, by wenzelm
tuned;
2012-10-03, by wenzelm
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
2012-10-03, by wenzelm
printed "_ofsort" is subject to show_markup as well;
2012-10-03, by wenzelm
allow position constraints to coexist with 0 or 1 sort constraints;
2012-10-03, by wenzelm
made tactic more robust (less usage of stac)
2012-10-02, by traytel
continued changing type of corec type
2012-10-02, by blanchet
removed dead params and dead code
2012-10-02, by blanchet
changed type of corecursor for the nested recursion case
2012-10-02, by blanchet
made (co)rec tactic more robust when the simplifier succeeds early
2012-10-02, by blanchet
tuned;
2012-10-01, by wenzelm
removed unused module Blob;
2012-10-01, by wenzelm
more direct message header: eliminated historic encoding via single letter;
2012-10-01, by wenzelm
tuned whitespace;
2012-10-01, by wenzelm
tuned proofs;
2012-10-01, by wenzelm
report sort assignment of visible type variables;
2012-10-01, by wenzelm
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
2012-10-01, by wenzelm
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
2012-10-01, by blanchet
tweaked corecursor/coiterator tactic
2012-10-01, by blanchet
changed the type of the recursor for nested recursion
2012-10-01, by blanchet
fixed quick-and-dirty mode
2012-09-30, by blanchet
tuning
2012-09-30, by blanchet
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
2012-09-30, by traytel
got rid of subst_tac alias
2012-09-30, by traytel
tuned tactic
2012-09-30, by traytel
tuned proofs;
2012-09-29, by wenzelm
tuned proofs;
2012-09-29, by wenzelm
proper handling of constraints stemming from idtyp_ast_tr';
2012-09-29, by wenzelm
enable show_markup by default (approx. double output size);
2012-09-29, by wenzelm
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-29, by wenzelm
explicit show_types takes preferenced over show_markup;
2012-09-29, by wenzelm
ignore wrapped markup elements in Proof General;
2012-09-29, by wenzelm
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
2012-09-29, by wenzelm
treat wrapped markup elements as raw markup delimiters;
2012-09-29, by wenzelm
tuned signature;
2012-09-29, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
tuned;
2012-09-28, by wenzelm
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28, by wenzelm
merged
2012-09-28, by wenzelm
eliminated dead code;
2012-09-28, by wenzelm
smarter handling of tracing messages;
2012-09-28, by wenzelm
display number of tracing messages;
2012-09-28, by wenzelm
tuned signature;
2012-09-28, by wenzelm
tuned proofs;
2012-09-28, by wenzelm
simplified simpset
2012-09-28, by blanchet
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28, by blanchet
tuned tactic
2012-09-28, by traytel
updated keywords using proper "isabelle update_keywords";
2012-09-28, by wenzelm
tuned tactic
2012-09-28, by traytel
tuned tactic
2012-09-28, by traytel
merge
2012-09-28, by blanchet
renamed ML file in preparation for next step
2012-09-28, by blanchet
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28, by blanchet
modernized example, exploiting "rep_compat" option
2012-09-28, by blanchet
compatibility option to use "rep_datatype"
2012-09-28, by blanchet
tuned message
2012-09-28, by blanchet
modernized example
2012-09-28, by blanchet
tuned tactics
2012-09-28, by traytel
second usage of const_typ
2012-09-28, by nipkow
new antiquotation const_typ
2012-09-28, by nipkow
tuned printing of _ in latex
2012-09-28, by nipkow
mk_readable_rsp_thm_eq is more robust now
2012-09-27, by kuncar
new get function for non-symmetric relator_eq & tuned
2012-09-27, by kuncar
merged
2012-09-27, by wenzelm
tuned tactic; got rid of substs_tac alias
2012-09-27, by traytel
use a nicer scheme to indexify names
2012-09-27, by blanchet
tuned tactic
2012-09-27, by traytel
type of the bound of a BNF depends at most on dead type variables
2012-09-27, by traytel
repaired signature
2012-09-27, by blanchet
lower the defaults for the number of bits, based on an example by Lukas Bulwahn
2012-09-27, by blanchet
modernized examples
2012-09-27, by blanchet
merged
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
operations to turn markup into XML;
2012-09-27, by wenzelm
removed obsolete org.w3c.dom operations;
2012-09-27, by wenzelm
eliminated obsolete HTML/CSS functionality;
2012-09-27, by wenzelm
removed obsolete Output1 dockable;
2012-09-27, by wenzelm
physical File.eq in conformance to Isabelle/ML;
2012-09-27, by wenzelm
tuned proofs;
2012-09-27, by wenzelm
tuned;
2012-09-27, by wenzelm
updated to consolidated SortedMap in scala-2.9.x;
2012-09-27, by wenzelm
partly ported "TreeFI" example to new syntax
2012-09-27, by blanchet
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
2012-09-27, by blanchet
tuned
2012-09-27, by nipkow
tuned
2012-09-27, by nipkow
merge
2012-09-27, by blanchet
modernized examples;
2012-09-27, by blanchet
some support for jEdit warmstart;
2012-09-26, by wenzelm
discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-09-26, by wenzelm
tuned message;
2012-09-26, by wenzelm
merged
2012-09-26, by wenzelm
disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
2012-09-26, by blanchet
got rid of other instance of shaky "Thm.generalize"
2012-09-26, by blanchet
tweaked theorem names (in particular, dropped s's)
2012-09-26, by blanchet
get rid of shaky "Thm.generalize"
2012-09-26, by blanchet
fixed "rels" + split them into injectivity and distinctness
2012-09-26, by blanchet
generate high-level "coinduct" and "strong_coinduct" properties
2012-09-26, by blanchet
added coinduction tactic
2012-09-26, by blanchet
generalized tactic a bit
2012-09-26, by blanchet
export "dtor_map_coinduct" theorems, since they're used in one example
2012-09-26, by blanchet
name tuning
2012-09-26, by blanchet
parameterized "subst_tac"
2012-09-26, by blanchet
generate high-level "maps", "sets", and "rels" properties
2012-09-26, by blanchet
use singular since there is always only one theorem
2012-09-26, by blanchet
nicer type var names
2012-09-26, by blanchet
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
2012-09-26, by blanchet
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
2012-09-26, by blanchet
leave out some internal theorems unless "bnf_note_all" is set
2012-09-26, by blanchet
tuned
2012-09-26, by nipkow
added counterexamples
2012-09-26, by nipkow
tuned
2012-09-26, by nipkow
tuned
2012-09-25, by nipkow
more uniform graphview terminology;
2012-09-26, by wenzelm
proper Symbol.decode -- especially relevant for Proof General;
2012-09-26, by wenzelm
suppress empty tooltips;
2012-09-26, by wenzelm
obsolete;
2012-09-26, by wenzelm
updated keywords;
2012-09-26, by wenzelm
more uniform graphview terminology;
2012-09-26, by wenzelm
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
2012-09-26, by wenzelm
proper install_fonts;
2012-09-26, by wenzelm
proper jvmpath for Windows;
2012-09-25, by wenzelm
basic integration of graphview into document model;
2012-09-25, by wenzelm
ML support for generic graph display, with browser and graphview backends (via print modes);
2012-09-25, by wenzelm
tuned;
2012-09-25, by wenzelm
more complete build;
2012-09-25, by wenzelm
proper error message;
2012-09-25, by wenzelm
separate module Graph_Display;
2012-09-25, by wenzelm
added graph encode/decode operations;
2012-09-25, by wenzelm
tuned;
2012-09-25, by wenzelm
minimal component and build setup for graphview;
2012-09-24, by wenzelm
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
2012-09-24, by Markus Kaiser
made smlnj even happier
2012-09-24, by haftmann
tuned proofs;
2012-09-24, by wenzelm
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
2012-09-24, by wenzelm
updated checksum, which appears to have changed accidentally;
2012-09-24, by wenzelm
updated to exec_process-1.0.2;
2012-09-24, by wenzelm
search bash via PATH as usual (this is no longer restricted to Cygwin with its known file-system layout);
2012-09-24, by wenzelm
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
2012-09-24, by wenzelm
Mirabelle appears to work better in single-threaded mode;
2012-09-24, by wenzelm
generalized types
2012-09-24, by nipkow
tuned termination proof
2012-09-24, by nipkow
adapted examples to new names
2012-09-23, by blanchet
renamed coinduction principles to have "dtor" in the name
2012-09-23, by blanchet
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
2012-09-23, by blanchet
renamed "map_simps" to "{c,d}tor_maps"
2012-09-23, by blanchet
took out accidentally submitted "tracing" calls
2012-09-23, by blanchet
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
2012-09-23, by blanchet
simplified fact policies
2012-09-23, by blanchet
generate "rel_as_srel" and "rel_flip" properties
2012-09-23, by blanchet
started work on generation of "rel" theorems
2012-09-23, by blanchet
make smlnj happy
2012-09-23, by haftmann
more strict typscheme_equiv check: must fix variables of more specific type;
2012-09-22, by haftmann
cache should not contain material from descendant theory
2012-09-22, by haftmann
some PIDE NEWS from this summer;
2012-09-22, by wenzelm
tuned whitespace;
2012-09-22, by wenzelm
tuned;
2012-09-22, by wenzelm
tuned proofs;
2012-09-22, by wenzelm
report proper binding positions only -- avoid swamping document model with unspecific information;
2012-09-22, by wenzelm
accumulate under exec_id as well;
2012-09-22, by wenzelm
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
2012-09-22, by wenzelm
misc tuning;
2012-09-22, by wenzelm
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
2012-09-22, by wenzelm
tuned signature;
2012-09-22, by wenzelm
tuned proofs;
2012-09-21, by wenzelm
misc tuning;
2012-09-21, by wenzelm
tighten margin for TextArea instead of Lobo;
2012-09-21, by wenzelm
misc tuning;
2012-09-21, by wenzelm
renamed LFP low-level rel property to have ctor not dtor in its name
2012-09-21, by blanchet
changed base session for "HOL-BNF" for faster building in the typical case
2012-09-21, by blanchet
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
2012-09-21, by blanchet
fixed a few names that escaped the renaming
2012-09-21, by blanchet
tuned whitespace
2012-09-21, by blanchet
merged
2012-09-21, by wenzelm
clean up lemmas used for composition
2012-09-21, by blanchet
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
2012-09-21, by blanchet
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-21, by blanchet
renamed top-level theory from "Codatatype" to "BNF"
2012-09-21, by blanchet
adapted examples to renamings
2012-09-21, by blanchet
renamed "pred" to "rel" (relator)
2012-09-21, by blanchet
renamed "rel" to "srel"
2012-09-21, by blanchet
fixed bug introduced by fold/unfold renaming
2012-09-21, by blanchet
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
2012-09-21, by blanchet
simplified code
2012-09-21, by blanchet
tuned a few ML names
2012-09-21, by blanchet
renamed "fld"/"unf" to "ctor"/"dtor"
2012-09-21, by blanchet
tuning
2012-09-21, by blanchet
renamed "upto" coinduction "strong"
2012-09-21, by blanchet
tuned variable names
2012-09-21, by blanchet
tuned names
2012-09-21, by nipkow
more termination proofs
2012-09-21, by nipkow
rel_Gr does not depend on map_wpull
2012-09-21, by traytel
renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
2012-09-21, by wenzelm
more realistic sendback: pick exec_id from message position and text from buffer;
2012-09-21, by wenzelm
some support for hovering and sendback area;
2012-09-21, by wenzelm
merged
2012-09-21, by wenzelm
tuned antiquotations
2012-09-21, by traytel
merged
2012-09-21, by wenzelm
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
2012-09-21, by traytel
conected CS to big-step
2012-09-21, by nipkow
generate "expand" property
2012-09-21, by blanchet
merge
2012-09-20, by blanchet
finished "disc_coiter_iff" etc. generation
2012-09-20, by blanchet
the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
2012-09-20, by blanchet
generate coiter_iff and corec_iff theorems
2012-09-20, by blanchet
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
2012-09-20, by Andreas Lochbihler
more efficient code setup
2012-09-20, by Andreas Lochbihler
added "simp"s to coiter/corec theorems + export under "simps" name
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
tuned
2012-09-20, by nipkow
less rendering (cf. 28bd0709443a) -- avoid conflict with static token markup of different keyword kinds;
2012-09-21, by wenzelm
tuned painter;
2012-09-20, by wenzelm
clarified message background;
2012-09-20, by wenzelm
tuned rendering;
2012-09-20, by wenzelm
no caret painting;
2012-09-20, by wenzelm
text_rendering as managed task, with cancellation;
2012-09-20, by wenzelm
more management of Invoke_Scala tasks;
2012-09-20, by wenzelm
more direct Markup_Tree.from_XML;
2012-09-20, by wenzelm
tuned signature;
2012-09-20, by wenzelm
more direct Markup_Tree.from_XML;
2012-09-20, by wenzelm
tuned signature;
2012-09-20, by wenzelm
tuned;
2012-09-20, by wenzelm
removed lpfp and proved least pfp thm
2012-09-20, by nipkow
provide predicator, define relator
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
adapting "More_BNFs" to new relators/predicators
2012-09-20, by blanchet
fixed infinite loop with trivial rel_O_Gr + tuning
2012-09-20, by blanchet
adapted FP code to new relator approach
2012-09-20, by blanchet
tuning
2012-09-20, by blanchet
renamed "bnf_fp_util.ML" to "bnf_fp.ML"
2012-09-20, by blanchet
adapted BNF composition to new relator approach
2012-09-20, by blanchet
don't define relators unless necessary
2012-09-20, by blanchet
moved predicator definition before after_qed
2012-09-20, by blanchet
add rel as first-class citizen of BNF
2012-09-20, by blanchet
renamed "rel_def" to "rel_O_Gr"
2012-09-20, by blanchet
renamed "sum_setl" to "setl" and similarly for r
2012-09-20, by blanchet
tuned ID/DEADID setup
2012-09-20, by blanchet
JavaFX is inactive by default;
2012-09-19, by wenzelm
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
2012-09-19, by wenzelm
universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
2012-09-19, by wenzelm
more direct GUI component;
2012-09-19, by wenzelm
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-19, by wenzelm
made SML/NJ happy;
2012-09-19, by wenzelm
tuned;
2012-09-19, by wenzelm
merged
2012-09-19, by wenzelm
recording elapsed time in mutabelle for more detailed evaluation
2012-09-19, by bulwahn
Added missing predicators (for multisets and countable sets)
2012-09-18, by popescua
added top-level theory for Cardinals
2012-09-18, by popescua
group "simps" together
2012-09-18, by blanchet
register induct attributes
2012-09-18, by blanchet
further tuned simpset
2012-09-18, by blanchet
bnf_note_all mode for "pre_"-BNFs
2012-09-18, by traytel
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
2012-09-18, by traytel
tuned
2012-09-18, by nipkow
beautified names
2012-09-18, by nipkow
proved all upper bounds
2012-09-18, by nipkow
tuned simpset
2012-09-17, by blanchet
cleaner way of dealing with the set functions of sums and products
2012-09-17, by blanchet
handle the general case with more than two levels of nesting when discharging induction prem prems
2012-09-17, by blanchet
clean unfolding of prod and sum sets
2012-09-17, by blanchet
got rid of one "auto" in induction tactic
2012-09-17, by blanchet
cleaned up internal naming scheme for bnfs
2012-09-17, by traytel
more robust GUI component handlers;
2012-09-19, by wenzelm
more rendering;
2012-09-18, by wenzelm
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
2012-09-18, by wenzelm
output is read-only;
2012-09-18, by wenzelm
token marker for extended syntax styles;
2012-09-18, by wenzelm
pass base_snapshot to enable hyperlinks into other nodes;
2012-09-18, by wenzelm
more explicit message markup and rendering;
2012-09-18, by wenzelm
recover order of stacked markup;
2012-09-18, by wenzelm
some actual rich text markup via XML.content_markup;
2012-09-18, by wenzelm
proper separation of output messages;
2012-09-18, by wenzelm
some support for inital command markup;
2012-09-18, by wenzelm
more static rendering state;
2012-09-18, by wenzelm
Pretty_Text_Area is based on Rich_Text_Area;
2012-09-18, by wenzelm
renamed Text_Area_Painter to Rich_Text_Area;
2012-09-17, by wenzelm
tuned signature -- more general Text_Area_Painter operations;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
tuned signature;
2012-09-17, by wenzelm
somewhat more general JEdit_Lib;
2012-09-17, by wenzelm
prefer official polyml-5.5.0;
2012-09-17, by wenzelm
bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;
2012-09-17, by wenzelm
merged
2012-09-17, by wenzelm
tuned
2012-09-17, by nipkow
updated to polyml-5.5.0;
2012-09-17, by wenzelm
some updates for polyml-5.5.0;
2012-09-17, by wenzelm
tuned
2012-09-17, by nipkow
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
2012-09-16, by wenzelm
got rid of ad-hoc lift function
2012-09-16, by nipkow
converted wt into a set, tuned names
2012-09-16, by nipkow
use strip_typeN in bnf_def (instead of repairing strip_type)
2012-09-16, by traytel
removing find_theorems commands that were left in the developments accidently
2012-09-16, by bulwahn
tuning
2012-09-15, by blanchet
tuned code to avoid special case for "fun"
2012-09-15, by blanchet
tuned induction tactic
2012-09-15, by blanchet
tuned error message
2012-09-15, by blanchet
tuning
2012-09-15, by blanchet
typeclass formalising bounded subtraction
2012-09-15, by haftmann
dropped some unused identifiers
2012-09-15, by haftmann
export rel_mono theorem
2012-09-15, by traytel
merged two unfold steps
2012-09-14, by blanchet
took out one rotate_tac
2012-09-14, by blanchet
killed spurious rotate_tac; use auto instead of blast
2012-09-14, by blanchet
moved blast tactic to where it is actually needed
2012-09-14, by blanchet
fixed bug in "mk_map" for the "fun" case
2012-09-14, by blanchet
correct generalization to 3 or more mutually recursive datatypes
2012-09-14, by blanchet
provide more guidance, exploiting our knowledge of the goal
2012-09-14, by blanchet
fixed issue with bound variables in prem prems + tuning
2012-09-14, by blanchet
use right version of "mk_UnIN"
2012-09-14, by blanchet
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14, by blanchet
tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14, by blanchet
tuned proofs;
2012-09-14, by wenzelm
merged
2012-09-14, by wenzelm
polished the induction
2012-09-14, by blanchet
put the flat at the right place (to avoid exceptions)
2012-09-14, by blanchet
fixed variable exporting problem
2012-09-14, by blanchet
compile
2012-09-14, by blanchet
added induct tactic
2012-09-14, by blanchet
tuning
2012-09-14, by blanchet
renamed "mk_UnN" to "mk_UnIN"
2012-09-14, by blanchet
merged two commands
2012-09-14, by blanchet
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
2012-09-14, by blanchet
distinguish between nested and nesting BNFs
2012-09-14, by blanchet
make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14, by blanchet
derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
2012-09-14, by blanchet
no longer react on global_settings (cf. 34ac36642a31);
2012-09-14, by wenzelm
refined output panel: more value-oriented approach to update and caret focus;
2012-09-14, by wenzelm
clarified markup names;
2012-09-14, by wenzelm
more general Document_Model.point_range;
2012-09-14, by wenzelm
more static handling of rendering options;
2012-09-14, by wenzelm
tuned options (again);
2012-09-14, by wenzelm
more scalable option-group;
2012-09-14, by wenzelm
tuned
2012-09-14, by nipkow
merged
2012-09-13, by wenzelm
tuned proofs;
2012-09-13, by wenzelm
remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced
2012-09-13, by hoelzl
workaround for HOL-Mirabelle-ex oddities;
2012-09-13, by wenzelm
instructions for quick start in 20min;
2012-09-13, by wenzelm
more liberal init_components: base dir may get created later when resolving missing components;
2012-09-13, by wenzelm
more efficient painting based on cached result;
2012-09-13, by wenzelm
more standard init_components -- particularly important to pick up correct jdk/scala version;
2012-09-13, by wenzelm
tuned
2012-09-13, by nipkow
merged
2012-09-12, by wenzelm
rough and ready induction
2012-09-12, by blanchet
nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
2012-09-12, by blanchet
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-09-12, by wenzelm
eliminated some old material that is unused in the visible universe;
2012-09-12, by wenzelm
tuning
2012-09-12, by blanchet
set up things for (co)induction sugar
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
added sumEN_tupled_balanced
2012-09-12, by blanchet
load fonts into JavaFX as well;
2012-09-12, by wenzelm
some support for actual HTML rendering;
2012-09-12, by wenzelm
merged
2012-09-12, by wenzelm
free variable name tuning
2012-09-12, by blanchet
reuse generated names (they look better + slightly more efficient)
2012-09-12, by blanchet
desambiguate grammar (e.g. for Nil's mixfix ("[]"))
2012-09-12, by blanchet
avoided duplicate lemma
2012-09-12, by blanchet
put an underscore between names, for compatibility with old package (and also because it makes sense)
2012-09-12, by blanchet
got rid of metis calls
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-12, by wenzelm
standardized ML aliases;
2012-09-12, by wenzelm
tuned headers;
2012-09-12, by wenzelm
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
2012-09-12, by wenzelm
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
2012-09-12, by wenzelm
more robust interrupt handling;
2012-09-12, by wenzelm
some attempts to synchronize ROOT/files and document/build;
2012-09-12, by wenzelm
tuned error;
2012-09-12, by wenzelm
option_pred characterization
2012-09-12, by traytel
true vs. True in pattern matching
2012-09-12, by traytel
reduced theory dependencies
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
moved theorems closer to where they are used
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
renamed "Ordinals_and_Cardinals" to "Cardinals"
2012-09-12, by blanchet
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
2012-09-12, by blanchet
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
tuning annotations
2012-09-12, by blanchet
tuned antiquotations
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
added optional qualifiers for constructors and destructors, similarly to the old package
2012-09-12, by blanchet
adapted example
2012-09-12, by blanchet
added attributes to theorems
2012-09-12, by blanchet
merged
2012-09-11, by wenzelm
support for sort constraints in new (co)data commands
2012-09-11, by blanchet
provide a programmatic interface for FP sugar
2012-09-11, by blanchet
some GUI support for color options;
2012-09-11, by wenzelm
more precise sections;
2012-09-11, by wenzelm
provide color values via options;
2012-09-11, by wenzelm
prefer tuning parameters as public methods (again) -- to allow overriding in applications;
2012-09-11, by wenzelm
updated keywords;
2012-09-11, by wenzelm
merged
2012-09-11, by wenzelm
tuned;
2012-09-11, by wenzelm
more informative tooltip: default value;
2012-09-11, by wenzelm
more options;
2012-09-11, by wenzelm
allow defaults for one datatype to involve the constructor of another one in the mutually recursive case
2012-09-11, by blanchet
added "defaults" option
2012-09-11, by blanchet
removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
2012-09-11, by blanchet
spin off "bnf_def_tactics.ML"
2012-09-11, by blanchet
move "bnf_util.ML" to "BNF_Util.thy"
2012-09-11, by blanchet
renamed "BNF_Library" to "BNF_Util"
2012-09-11, by blanchet
generate all sel theorems
2012-09-11, by blanchet
allow default values for selectors in low-level "wrap_data" command
2012-09-11, by blanchet
removed needless "infer_types" call
2012-09-11, by blanchet
added no_dests option
2012-09-11, by blanchet
tuning
2012-09-11, by blanchet
finished splitting sum types for corecursors
2012-09-11, by blanchet
split sum types in corecursor definition
2012-09-11, by blanchet
first step towards splitting corecursor function arguments into (p, g, h) triples
2012-09-11, by blanchet
reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced
2012-09-11, by blanchet
replaced jedit_relative_font_size by jedit_font_scale;
2012-09-11, by wenzelm
need to provide label via some jEdit property;
2012-09-11, by wenzelm
some support to organize options in sections;
2012-09-11, by wenzelm
merged
2012-09-11, by wenzelm
generate "id" rather than (%v. v)
2012-09-11, by blanchet
correctly generate sel_coiter and sel_corec theorems
2012-09-11, by blanchet
generate "sel_coiters" and friends
2012-09-10, by blanchet
sanity check
2012-09-10, by blanchet
implemented and use "mk_sum_casesN_balanced"
2012-09-10, by blanchet
fixed general case of "mk_sumEN_balanced"
2012-09-10, by blanchet
debug
2012-09-10, by blanchet
fixed base case of "mk_sumEN_balanced"
2012-09-10, by blanchet
prevent inconsistent selector types
2012-09-10, by blanchet
minor optimization
2012-09-10, by blanchet
allow same selector name for several constructors
2012-09-10, by blanchet
removed done TODO
2012-09-10, by blanchet
avoid type inference + tuning
2012-09-10, by blanchet
use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-10, by blanchet
busted -- let's use more neutral names
2012-09-10, by blanchet
replacing own dummy value by Haskell's Prelude.undefined
2012-09-10, by bulwahn
prefer global default font over IsabelleText of jEdit TextArea;
2012-09-11, by wenzelm
uniform operation on initial delay;
2012-09-11, by wenzelm
option jedit_load_delay;
2012-09-10, by wenzelm
dynamic evaluation of time (e.g. via options);
2012-09-10, by wenzelm
proper multi-line tooltip;
2012-09-10, by wenzelm
more detailed option tooltip;
2012-09-10, by wenzelm
more systematic JEdit_Options.make_component;
2012-09-10, by wenzelm
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
2012-09-10, by wenzelm
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-09-10, by wenzelm
more explicit indication of legacy features;
2012-09-10, by wenzelm
more explicit indication of legacy features;
2012-09-10, by wenzelm
simplify "Process" example even further
2012-09-10, by traytel
stabilized generation of parameterized theorem
2012-09-10, by traytel
added snippets
2012-09-10, by nipkow
simplify "Process" example further
2012-09-09, by blanchet
simplify "Process" example
2012-09-09, by blanchet
full name of a type as key in bnf table
2012-09-09, by traytel
fixed bug with one-value codatatype "codata 'a dead_foo = A"
2012-09-09, by blanchet
tuning
2012-09-09, by blanchet
fixed and reenabled "corecs" theorems
2012-09-09, by blanchet
fixed and enabled generation of "coiters" theorems, including the recursive case
2012-09-09, by blanchet
generate "fld_unf_corecs" as well
2012-09-09, by blanchet
reactivated generation of "coiters" theorems
2012-09-09, by blanchet
use map_id, not map_id', to allow better composition
2012-09-09, by blanchet
open typedefs everywhere in the package
2012-09-09, by traytel
open typedef for datatypes
2012-09-09, by traytel
fixed and enabled iterator/recursor theorems
2012-09-08, by blanchet
renamed for consistency
2012-09-08, by blanchet
oops
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
2012-09-08, by blanchet
fixed bug with one-value types with phantom type arguments
2012-09-08, by blanchet
imported patch debugging
2012-09-08, by blanchet
repaired "nofail4" example
2012-09-08, by blanchet
renamed xxxBNF to pre_xxx
2012-09-08, by blanchet
fixed handling of map of "fun"
2012-09-08, by blanchet
comment out code that's not ready
2012-09-08, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip