bulwahn [Wed, 20 Jan 2010 14:09:46 +0100] rev 34951
merged
krauss [Mon, 18 Jan 2010 10:34:27 +0100] rev 34950
function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
bulwahn [Wed, 20 Jan 2010 14:05:17 +0100] rev 34949
merged
bulwahn [Wed, 20 Jan 2010 11:56:45 +0100] rev 34948
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
haftmann [Fri, 22 Jan 2010 13:39:00 +0100] rev 34947
simplified proofs
haftmann [Fri, 22 Jan 2010 13:38:40 +0100] rev 34946
NEWS
haftmann [Fri, 22 Jan 2010 13:38:29 +0100] rev 34945
more accurate dependencies
haftmann [Fri, 22 Jan 2010 13:38:28 +0100] rev 34944
code literals: distinguish numeral classes by different entries
haftmann [Fri, 22 Jan 2010 13:38:28 +0100] rev 34943
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann [Thu, 21 Jan 2010 09:27:57 +0100] rev 34942
merged
haftmann [Sat, 16 Jan 2010 17:15:28 +0100] rev 34941
dropped some old primrecs and some constdefs
haftmann [Sat, 16 Jan 2010 17:15:27 +0100] rev 34940
explicit CONST in translations
haftmann [Sat, 16 Jan 2010 17:15:27 +0100] rev 34939
modernized syntax
blanchet [Wed, 20 Jan 2010 11:54:19 +0100] rev 34938
fix issues with previous Nitpick change
blanchet [Wed, 20 Jan 2010 10:38:19 +0100] rev 34937
merged
blanchet [Wed, 20 Jan 2010 10:38:06 +0100] rev 34936
some work on Nitpick's support for quotient types;
quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"
blanchet [Thu, 14 Jan 2010 17:06:35 +0100] rev 34935
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
hoelzl [Tue, 19 Jan 2010 17:53:11 +0100] rev 34934
Added transpose_rectangle, when the input list is rectangular.
hoelzl [Tue, 19 Jan 2010 16:52:01 +0100] rev 34933
Add transpose to the List-theory.
wenzelm [Tue, 02 Feb 2010 21:37:27 +0100] rev 34932
some examples for basic context operations;
wenzelm [Tue, 02 Feb 2010 13:22:36 +0100] rev 34931
minimal tuning of this slightly dated material;
wenzelm [Tue, 02 Feb 2010 13:11:04 +0100] rev 34930
added Subgoal.FOCUS;
misc tuning and clarification;
wenzelm [Tue, 02 Feb 2010 12:37:57 +0100] rev 34929
misc tuning and clarification;
wenzelm [Tue, 02 Feb 2010 11:47:49 +0100] rev 34928
moved examples to proper place;
wenzelm [Mon, 01 Feb 2010 22:46:12 +0100] rev 34927
more details on long names, binding/naming, name space;
tuned;
wenzelm [Sun, 31 Jan 2010 22:08:25 +0100] rev 34926
Variable.names_of;
tuned;
wenzelm [Sun, 31 Jan 2010 21:40:44 +0100] rev 34925
more details on Isabelle symbols;
wenzelm [Fri, 29 Jan 2010 23:59:03 +0100] rev 34924
theory data example;
wenzelm [Fri, 29 Jan 2010 23:57:57 +0100] rev 34923
basic setup for ML examples: tag "mlex";
wenzelm [Thu, 28 Jan 2010 22:39:48 +0100] rev 34922
tuned signature;
wenzelm [Thu, 28 Jan 2010 22:38:11 +0100] rev 34921
formal markup of type aliases;
updated/tuned/clarified contexts;
misc tuning and clarification;
wenzelm [Thu, 28 Jan 2010 22:19:27 +0100] rev 34920
make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
wenzelm [Sat, 16 Jan 2010 21:14:15 +0100] rev 34919
Netbeans Library "Scala-compiler";
berghofe [Fri, 15 Jan 2010 19:14:51 +0100] rev 34918
union is an abbreviation for sup.
berghofe [Fri, 15 Jan 2010 14:43:00 +0100] rev 34917
merged
berghofe [Fri, 15 Jan 2010 13:37:41 +0100] rev 34916
Eliminated is_open option of Rule_Cases.make_nested/make_common;
use Rule_Cases.internalize_params to rename parameters instead.
berghofe [Sun, 10 Jan 2010 18:43:45 +0100] rev 34915
Adapted to changes in induct method.
berghofe [Sun, 10 Jan 2010 18:41:07 +0100] rev 34914
Adapted to changes in setup of induct method.
berghofe [Sun, 10 Jan 2010 18:39:50 +0100] rev 34913
Expand proofs of induct_atomize'/rulify'.
berghofe [Sun, 10 Jan 2010 18:37:37 +0100] rev 34912
Changed case names of converse_rtranclp_induct.
berghofe [Sun, 10 Jan 2010 18:11:00 +0100] rev 34911
Injectivity / distinctness theorems are now used to simplify induction rules.
berghofe [Sun, 10 Jan 2010 18:09:11 +0100] rev 34910
same_append_eq / append_same_eq are now used for simplifying induction rules.
berghofe [Sun, 10 Jan 2010 18:06:30 +0100] rev 34909
Tuned some proofs; nicer case names for some of the induction / cases rules.
berghofe [Sun, 10 Jan 2010 18:03:20 +0100] rev 34908
Added setup for simplification of equality constraints in induction rules.
berghofe [Sun, 10 Jan 2010 18:01:04 +0100] rev 34907
Added infrastructure for simplifying equality constraints.
Option (no_simp) restores old behaviour of induct method.
haftmann [Fri, 15 Jan 2010 08:27:21 +0100] rev 34906
spurious proof failure
haftmann [Thu, 14 Jan 2010 18:44:22 +0100] rev 34905
merged
haftmann [Thu, 14 Jan 2010 18:42:15 +0100] rev 34904
merged
haftmann [Thu, 14 Jan 2010 17:54:55 +0100] rev 34903
dropped unused binding
haftmann [Thu, 14 Jan 2010 17:54:54 +0100] rev 34902
dedicated conversions to and from Int
haftmann [Thu, 14 Jan 2010 17:47:39 +0100] rev 34901
printing of cases
haftmann [Thu, 14 Jan 2010 17:47:39 +0100] rev 34900
tuned for products vs. tupled functions
haftmann [Thu, 14 Jan 2010 17:47:39 +0100] rev 34899
added Scala setup
haftmann [Thu, 14 Jan 2010 17:47:38 +0100] rev 34898
allow individual printing of numerals during code serialization
blanchet [Thu, 14 Jan 2010 15:06:38 +0100] rev 34897
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
haftmann [Thu, 14 Jan 2010 09:18:08 +0100] rev 34896
adjusted to changes in code equation administration
haftmann [Wed, 13 Jan 2010 12:20:37 +0100] rev 34895
explicit abstract type of code certificates
haftmann [Wed, 13 Jan 2010 10:18:45 +0100] rev 34894
corrected error messages; tuned
haftmann [Wed, 13 Jan 2010 10:18:45 +0100] rev 34893
function transformer preprocessor applies to both code generators
haftmann [Wed, 13 Jan 2010 09:13:30 +0100] rev 34892
merged
haftmann [Tue, 12 Jan 2010 16:27:42 +0100] rev 34891
code certificates as integral part of code generation
haftmann [Wed, 13 Jan 2010 09:02:47 +0100] rev 34890
import of antiquote_setup not necessary
haftmann [Wed, 13 Jan 2010 08:56:25 +0100] rev 34889
merged
haftmann [Wed, 13 Jan 2010 08:56:16 +0100] rev 34888
being more accurate wrt. list syntax
haftmann [Wed, 13 Jan 2010 08:56:16 +0100] rev 34887
deactivate pretty code test for Scala -- no proper setup yet
haftmann [Wed, 13 Jan 2010 08:56:15 +0100] rev 34886
some syntax setup for Scala
wenzelm [Wed, 13 Jan 2010 00:08:56 +0100] rev 34885
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm [Tue, 12 Jan 2010 22:53:18 +0100] rev 34884
merged
paulson [Tue, 12 Jan 2010 16:55:59 +0000] rev 34883
Parsing errors during proof reconstruction now give rise to an intelligible error message.
wenzelm [Tue, 12 Jan 2010 22:23:29 +0100] rev 34882
rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs;
misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;
wenzelm [Tue, 12 Jan 2010 17:06:36 +0100] rev 34881
tuned initial properties/perspective;
wenzelm [Tue, 12 Jan 2010 16:51:51 +0100] rev 34880
provide JEDIT_SETTINGS via settings;
provide default perspective;
tuned default properties;
wenzelm [Tue, 12 Jan 2010 14:57:29 +0100] rev 34879
updated version and dependencies;
wenzelm [Tue, 12 Jan 2010 13:36:01 +0100] rev 34878
recovered subscript (cf. ded5b770ec1c);
haftmann [Tue, 12 Jan 2010 09:59:45 +0100] rev 34877
formal antiquotations for ML snippets; no "open" unsynchronized references
wenzelm [Mon, 11 Jan 2010 23:41:06 +0100] rev 34876
clarified terminology;
wenzelm [Mon, 11 Jan 2010 23:11:31 +0100] rev 34875
merged
haftmann [Mon, 11 Jan 2010 16:45:02 +0100] rev 34874
added code certificates
haftmann [Mon, 11 Jan 2010 16:45:02 +0100] rev 34873
tuned code equations
hoelzl [Mon, 11 Jan 2010 11:47:38 +0100] rev 34872
Matrices form a semiring with 0
wenzelm [Mon, 11 Jan 2010 23:00:05 +0100] rev 34871
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm [Mon, 11 Jan 2010 22:44:21 +0100] rev 34870
ignore some src/Tools/jEdit stuff;
wenzelm [Mon, 11 Jan 2010 22:31:27 +0100] rev 34869
merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b
wenzelm [Mon, 11 Jan 2010 22:01:39 +0100] rev 34868
more timing;
wenzelm [Mon, 11 Jan 2010 20:51:58 +0100] rev 34867
more tobust treatment of Document.current_state;
some timing;
wenzelm [Mon, 11 Jan 2010 18:28:31 +0100] rev 34866
new unparsed span for text right after existing command;
tuned;
wenzelm [Mon, 11 Jan 2010 18:26:38 +0100] rev 34865
Outer_Lex.is_ignored;
wenzelm [Mon, 11 Jan 2010 18:26:13 +0100] rev 34864
simplified Text_Edit;
wenzelm [Mon, 11 Jan 2010 16:49:11 +0100] rev 34863
eliminated strange mutable var commands;
removed_commands: refer to old commands;
misc tuning;
wenzelm [Mon, 11 Jan 2010 13:58:51 +0100] rev 34862
updated header;
wenzelm [Mon, 11 Jan 2010 13:55:32 +0100] rev 34861
eliminated obsolete isabelle.proofdocument.Token;
wenzelm [Mon, 11 Jan 2010 12:17:47 +0100] rev 34860
do not override Command.hashCode -- which was inconsistent with eq anyway;
unparsed: no id, commands observe pointer equality;
actually invoke edit_commands;
more correct doc_edits;
tuned;
wenzelm [Mon, 11 Jan 2010 01:40:18 +0100] rev 34859
renamed Command.content to source;
reorganization of document parsing, using command spans etc. -- initial setup;
wenzelm [Sun, 10 Jan 2010 21:14:44 +0100] rev 34858
further tuning of command_start;
wenzelm [Sun, 10 Jan 2010 21:08:23 +0100] rev 34857
refrain from poking blink rate -- might get stuck in invisible state;
wenzelm [Sun, 10 Jan 2010 20:38:23 +0100] rev 34856
eliminated Command.stop, which tends to case duplicate traversal of commands;
wenzelm [Sun, 10 Jan 2010 20:14:21 +0100] rev 34855
iterators for ranges of commands/starts -- avoid extra array per document;
try/finally for saved_color;
misc tuning;
wenzelm [Sun, 10 Jan 2010 17:10:32 +0100] rev 34854
tuned document changes;
wenzelm [Sun, 10 Jan 2010 16:40:21 +0100] rev 34853
misc tuning and clarification of Document/Change;
wenzelm [Sun, 10 Jan 2010 15:42:31 +0100] rev 34852
adhoc reset of blink rate;
bind "console" instance;
wenzelm [Sun, 10 Jan 2010 15:15:04 +0100] rev 34851
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm [Sat, 09 Jan 2010 23:28:52 +0100] rev 34850
redirect scala.Console output during interpretation;
misc tuning;
wenzelm [Sat, 09 Jan 2010 22:03:47 +0100] rev 34849
bind "session";
added printInfoMessage;
added stop -- re-inits the interpreter;
wenzelm [Sat, 09 Jan 2010 22:02:35 +0100] rev 34848
export isabelle_system, e.g. for use via "session" in Isabelle/Scala interpreter;
wenzelm [Sat, 09 Jan 2010 21:31:59 +0100] rev 34847
removed unused var plugin;
wenzelm [Sat, 09 Jan 2010 18:25:48 +0100] rev 34846
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
reduced predefined values, which take time and are static anyway;
wenzelm [Sat, 09 Jan 2010 00:49:51 +0100] rev 34845
provide some bindings of jEdit values;
plain color for input;
wenzelm [Fri, 08 Jan 2010 12:26:44 +0100] rev 34844
more precise prompt etc.;
wenzelm [Fri, 08 Jan 2010 12:26:22 +0100] rev 34843
define scala.home, for more robust startup of Scala tools, notably the compiler;
wenzelm [Fri, 08 Jan 2010 12:25:37 +0100] rev 34842
added jEdit Console and Scala compiler;
wenzelm [Fri, 08 Jan 2010 00:47:10 +0100] rev 34841
some attempts at Scala console plugin;
wenzelm [Wed, 06 Jan 2010 23:46:00 +0100] rev 34840
more precise treatment of document/state assigment;
wenzelm [Tue, 05 Jan 2010 18:29:21 +0100] rev 34839
more precise notion of bad messages;
wenzelm [Tue, 05 Jan 2010 18:23:39 +0100] rev 34838
use Text_Edit provided by Isabelle;
wenzelm [Tue, 05 Jan 2010 18:23:15 +0100] rev 34837
result.is_ready is not bad;
wenzelm [Mon, 04 Jan 2010 19:42:35 +0100] rev 34836
singleton status messages, with more precise patterns -- report bad messages;
wenzelm [Mon, 04 Jan 2010 19:08:10 +0100] rev 34835
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
recent_document: require finished state assignment;
explicitly typed Session.lookup_command;
wenzelm [Mon, 04 Jan 2010 00:13:09 +0100] rev 34834
slightly more uniform/robust handling of visible document;
uniform changed_delay for view updates;
misc tuning;
wenzelm [Sun, 03 Jan 2010 23:03:04 +0100] rev 34833
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
Change.ancestors: frugal iterator;
wenzelm [Sun, 03 Jan 2010 20:50:07 +0100] rev 34832
more explicit treatment of command/document state;
misc tuning and clarification;