bulwahn [Wed, 28 Mar 2012 10:16:02 +0200] rev 47179
changing more definitions to quotient_definition
bulwahn [Wed, 28 Mar 2012 10:02:22 +0200] rev 47178
removing now redundant impl_of theorems in DAList
bulwahn [Wed, 28 Mar 2012 10:00:52 +0200] rev 47177
using abstract code equations for proofs of code equations in Multiset
wenzelm [Wed, 28 Mar 2012 12:08:08 +0200] rev 47176
simplified statements and proofs;
wenzelm [Wed, 28 Mar 2012 11:46:14 +0200] rev 47175
tuned whitespace;
wenzelm [Wed, 28 Mar 2012 11:17:32 +0200] rev 47174
updated Sign.add_type, Name_Space.declare;
wenzelm [Wed, 28 Mar 2012 11:04:39 +0200] rev 47173
updated comments;
huffman [Wed, 28 Mar 2012 08:25:51 +0200] rev 47172
merged
huffman [Tue, 27 Mar 2012 22:10:26 +0200] rev 47171
remove unnecessary rules from the simpset
huffman [Tue, 27 Mar 2012 21:58:41 +0200] rev 47170
remove unused premises
huffman [Tue, 27 Mar 2012 21:48:55 +0200] rev 47169
remove duplicate lemmas
huffman [Tue, 27 Mar 2012 21:48:26 +0200] rev 47168
mark some duplicate lemmas for deletion
huffman [Tue, 27 Mar 2012 20:19:23 +0200] rev 47167
remove more redundant lemmas
huffman [Tue, 27 Mar 2012 16:49:23 +0200] rev 47166
tuned proofs
huffman [Tue, 27 Mar 2012 19:21:05 +0200] rev 47165
remove redundant lemmas
huffman [Tue, 27 Mar 2012 16:04:51 +0200] rev 47164
generalized lemma zpower_zmod
huffman [Tue, 27 Mar 2012 15:53:48 +0200] rev 47163
remove redundant lemma
huffman [Tue, 27 Mar 2012 15:40:11 +0200] rev 47162
remove redundant lemma
huffman [Tue, 27 Mar 2012 15:34:36 +0200] rev 47161
remove duplicate [algebra] declarations
huffman [Tue, 27 Mar 2012 15:34:04 +0200] rev 47160
generalize more div/mod lemmas
huffman [Tue, 27 Mar 2012 15:27:49 +0200] rev 47159
generalize some theorems about div/mod
wenzelm [Wed, 28 Mar 2012 00:18:11 +0200] rev 47158
updated to jedit-4.5.1;
kuncar [Tue, 27 Mar 2012 17:58:53 +0200] rev 47157
merged
kuncar [Tue, 27 Mar 2012 14:46:34 +0200] rev 47156
note a code eqn in quotient_def
boehmes [Tue, 27 Mar 2012 17:11:02 +0200] rev 47155
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47154
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47153
fixed eta-extension of higher-order quantifiers in THF output
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47152
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47151
tuning
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47150
tuning (in particular, Symtab instead of AList)
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47149
tweak slices, based on eval by Daniel Wand
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47148
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47147
print a hint
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47146
avoid DL
blanchet [Tue, 27 Mar 2012 16:59:13 +0300] rev 47145
TFF: declare free types as types
bulwahn [Tue, 27 Mar 2012 15:34:04 +0200] rev 47144
merged
bulwahn [Tue, 27 Mar 2012 14:14:46 +0200] rev 47143
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
added remarks about further improvements
huffman [Tue, 27 Mar 2012 14:49:56 +0200] rev 47142
remove redundant lemmas
huffman [Tue, 27 Mar 2012 12:42:54 +0200] rev 47141
move int::ring_div instance upward, simplify several proofs
huffman [Tue, 27 Mar 2012 11:45:02 +0200] rev 47140
rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
huffman [Tue, 27 Mar 2012 11:41:16 +0200] rev 47139
extend definition of divmod_int_rel to handle denominator=0 case
huffman [Tue, 27 Mar 2012 11:02:18 +0200] rev 47138
tuned proofs
huffman [Tue, 27 Mar 2012 10:34:12 +0200] rev 47137
shorten a proof
huffman [Tue, 27 Mar 2012 10:20:31 +0200] rev 47136
simplify some proofs
huffman [Tue, 27 Mar 2012 09:54:39 +0200] rev 47135
rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
huffman [Tue, 27 Mar 2012 09:44:56 +0200] rev 47134
simplify some proofs
wenzelm [Mon, 26 Mar 2012 21:03:30 +0200] rev 47133
merged
nipkow [Mon, 26 Mar 2012 21:00:39 +0200] rev 47132
merged
nipkow [Mon, 26 Mar 2012 21:00:23 +0200] rev 47131
reverted to canonical name
wenzelm [Mon, 26 Mar 2012 20:45:59 +0200] rev 47130
merged
huffman [Mon, 26 Mar 2012 20:11:27 +0200] rev 47129
merged
huffman [Mon, 26 Mar 2012 20:09:18 +0200] rev 47128
revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
huffman [Mon, 26 Mar 2012 20:07:41 +0200] rev 47127
merged
huffman [Mon, 26 Mar 2012 20:07:29 +0200] rev 47126
fix incorrect code_modulename declarations
huffman [Mon, 26 Mar 2012 19:04:17 +0200] rev 47125
code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)
huffman [Mon, 26 Mar 2012 19:03:27 +0200] rev 47124
remove old-style semicolon
nipkow [Mon, 26 Mar 2012 20:09:52 +0200] rev 47123
merged
nipkow [Mon, 26 Mar 2012 18:54:41 +0200] rev 47122
Functions and lemmas by Christian Sternagel
wenzelm [Mon, 26 Mar 2012 20:42:00 +0200] rev 47121
more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;
wenzelm [Mon, 26 Mar 2012 19:18:03 +0200] rev 47120
disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
kuncar [Mon, 26 Mar 2012 18:32:22 +0200] rev 47119
tuned comment
kuncar [Mon, 26 Mar 2012 17:58:47 +0200] rev 47118
merged
kuncar [Mon, 26 Mar 2012 15:33:28 +0200] rev 47117
merged
kuncar [Mon, 26 Mar 2012 15:32:54 +0200] rev 47116
tuned proof - no smt call
wenzelm [Mon, 26 Mar 2012 16:25:08 +0200] rev 47115
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
wenzelm [Mon, 26 Mar 2012 15:38:09 +0200] rev 47114
updated theory header syntax and related details;
wenzelm [Sat, 24 Mar 2012 20:24:16 +0100] rev 47113
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
update for prospective jdk1.7.x component;
wenzelm [Mon, 26 Mar 2012 11:15:41 +0200] rev 47112
merged
blanchet [Mon, 26 Mar 2012 11:01:04 +0200] rev 47111
reintroduced broken proofs and regenerated certificates
wenzelm [Mon, 26 Mar 2012 10:56:56 +0200] rev 47110
merged, resolving trivial conflict;
blanchet [Mon, 26 Mar 2012 10:42:06 +0200] rev 47109
fixed Nitpick after numeral representation change (2a1953f0d20d)
huffman [Sun, 25 Mar 2012 20:15:39 +0200] rev 47108
merged fork with new numeral representation (see NEWS)
kuncar [Sat, 24 Mar 2012 16:27:04 +0100] rev 47107
merged
kuncar [Fri, 23 Mar 2012 22:00:17 +0100] rev 47106
use Thm.transfer for thms stored in generic context data storage
kuncar [Fri, 23 Mar 2012 18:23:47 +0100] rev 47105
hide invariant constant
wenzelm [Sat, 24 Mar 2012 12:28:45 +0100] rev 47104
explicit SMTP server (appears to be required after recent change of system configuration);
wenzelm [Sat, 24 Mar 2012 12:22:29 +0100] rev 47103
more isatest subscribers;
paulson [Fri, 23 Mar 2012 16:16:35 +0000] rev 47102
merged
paulson [Fri, 23 Mar 2012 16:16:15 +0000] rev 47101
proof tidying
kuncar [Mon, 16 Jan 2012 12:33:26 +0100] rev 47100
updated comment
kuncar [Fri, 23 Mar 2012 14:34:50 +0100] rev 47099
resolve invariant constant name clash
kuncar [Fri, 23 Mar 2012 14:29:29 +0100] rev 47098
update etc/isar-keywords.el
kuncar [Fri, 23 Mar 2012 14:26:09 +0100] rev 47097
fix example files
kuncar [Fri, 23 Mar 2012 14:25:31 +0100] rev 47096
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar [Fri, 23 Mar 2012 14:21:41 +0100] rev 47095
simplified code of generation of aggregate relations
kuncar [Fri, 23 Mar 2012 14:20:09 +0100] rev 47094
store the relational theorem for every relator
kuncar [Fri, 23 Mar 2012 14:18:43 +0100] rev 47093
store the quotient theorem for every quotient
kuncar [Fri, 23 Mar 2012 14:17:29 +0100] rev 47092
fix Quotient_Examples
kuncar [Fri, 23 Mar 2012 14:03:58 +0100] rev 47091
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
bulwahn [Fri, 23 Mar 2012 12:03:59 +0100] rev 47090
adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
wenzelm [Fri, 23 Mar 2012 20:32:43 +0100] rev 47089
tuned;
wenzelm [Thu, 22 Mar 2012 21:43:26 +0100] rev 47088
merged;
haftmann [Thu, 22 Mar 2012 18:54:39 +0100] rev 47087
fixed typo
haftmann [Thu, 22 Mar 2012 18:37:20 +0100] rev 47086
more instructive NEWS
paulson [Thu, 22 Mar 2012 17:52:50 +0000] rev 47085
more structured proofs
paulson [Thu, 22 Mar 2012 16:41:22 +0000] rev 47084
New Message
berghofe [Thu, 22 Mar 2012 10:10:02 +0100] rev 47083
No longer treat "title" as FDL keyword
wenzelm [Thu, 22 Mar 2012 16:44:19 +0100] rev 47082
tuned proofs;
wenzelm [Thu, 22 Mar 2012 15:41:49 +0100] rev 47081
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
uniform treatment of target contexts as invisible;
added Local_Theory.standard_form convenience;
wenzelm [Thu, 22 Mar 2012 11:11:51 +0100] rev 47080
tuned;
wenzelm [Thu, 22 Mar 2012 10:49:31 +0100] rev 47079
synchronize syntax uniformly for target stack and aux. context;
wenzelm [Thu, 22 Mar 2012 10:10:30 +0100] rev 47078
tuned;
wenzelm [Wed, 21 Mar 2012 23:41:22 +0100] rev 47077
merged
blanchet [Wed, 21 Mar 2012 16:53:24 +0100] rev 47076
removed Satallax option, now that this is the default
blanchet [Wed, 21 Mar 2012 16:53:24 +0100] rev 47075
doc update
blanchet [Wed, 21 Mar 2012 16:53:24 +0100] rev 47074
improve "remote_satallax" by exploiting unsat core
blanchet [Wed, 21 Mar 2012 16:53:24 +0100] rev 47073
generate weights and precedences for predicates as well
paulson [Wed, 21 Mar 2012 15:43:02 +0000] rev 47072
refinements to constructibility
paulson [Wed, 21 Mar 2012 13:05:40 +0000] rev 47071
More structured proofs for infinite cardinalities
wenzelm [Wed, 21 Mar 2012 23:41:58 +0100] rev 47070
actually expose target context;
wenzelm [Wed, 21 Mar 2012 23:26:35 +0100] rev 47069
more explicit Toplevel.open_target/close_target;
replaced 'context_includes' by 'context' 'includes';
tuned command descriptions;
wenzelm [Wed, 21 Mar 2012 21:24:13 +0100] rev 47068
tuned signature;
wenzelm [Wed, 21 Mar 2012 21:06:31 +0100] rev 47067
optional 'includes' element for long theorem statements;
tuned signatures;
wenzelm [Wed, 21 Mar 2012 17:25:35 +0100] rev 47066
basic support for nested contexts including bundles;
include multiple bundles;
renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML);
tuned signatures;
wenzelm [Wed, 21 Mar 2012 17:16:39 +0100] rev 47065
tuned messages;
wenzelm [Wed, 21 Mar 2012 15:19:45 +0100] rev 47064
basic support for nested local theory targets;
wenzelm [Wed, 21 Mar 2012 13:54:33 +0100] rev 47063
try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers;
wenzelm [Wed, 21 Mar 2012 11:36:47 +0100] rev 47062
improved isatest arguments for macbroy2;
wenzelm [Wed, 21 Mar 2012 11:25:19 +0100] rev 47061
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
tuned;
wenzelm [Wed, 21 Mar 2012 11:00:34 +0100] rev 47060
prefer explicitly qualified exception List.Empty;
wenzelm [Tue, 20 Mar 2012 21:37:31 +0100] rev 47059
merged
wenzelm [Tue, 20 Mar 2012 21:34:42 +0100] rev 47058
refined init_model: allow change of buffer name as caused by "Save as", for example;
avoid init_model while buffer.isLoading -- potentially prevent NPE of getText;
avoid emitting nested buffer.propertiesChanged events;
wenzelm [Tue, 20 Mar 2012 20:00:13 +0100] rev 47057
basic support for bundled declarations;
blanchet [Tue, 20 Mar 2012 18:42:45 +0100] rev 47056
doc update
blanchet [Tue, 20 Mar 2012 18:42:45 +0100] rev 47055
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet [Tue, 20 Mar 2012 18:42:45 +0100] rev 47054
removed obsolete temporary hack
blanchet [Tue, 20 Mar 2012 18:42:45 +0100] rev 47053
tweaks
paulson [Tue, 20 Mar 2012 17:20:33 +0000] rev 47052
proof tidying
wenzelm [Tue, 20 Mar 2012 18:01:34 +0100] rev 47051
minimalistic support for remote URLs: no master dir here;
blanchet [Tue, 20 Mar 2012 13:53:09 +0100] rev 47050
optimized "metis" call
blanchet [Tue, 20 Mar 2012 13:53:09 +0100] rev 47049
added term_order option to Mirabelle
blanchet [Tue, 20 Mar 2012 13:53:09 +0100] rev 47048
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
blanchet [Tue, 20 Mar 2012 13:53:09 +0100] rev 47047
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
blanchet [Tue, 20 Mar 2012 13:53:09 +0100] rev 47046
remove two options that were found to play hardly any role
blanchet [Tue, 20 Mar 2012 13:53:09 +0100] rev 47045
enable "metis_advisory_simp" by default
wenzelm [Tue, 20 Mar 2012 13:02:07 +0100] rev 47044
more stats;
paulson [Tue, 20 Mar 2012 11:03:46 +0000] rev 47043
merged
paulson [Tue, 20 Mar 2012 11:03:25 +0000] rev 47042
more structured proofs
blanchet [Tue, 20 Mar 2012 10:45:52 +0100] rev 47041
don't generate new SPASS constructs for old SPASS
blanchet [Tue, 20 Mar 2012 10:21:05 +0100] rev 47040
tune Metis example
blanchet [Tue, 20 Mar 2012 10:06:35 +0100] rev 47039
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47038
continued implementation of term ordering attributes
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47037
added "dont_preplay" alias
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47036
document "dont_preplay"
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47035
tuning
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47034
implement term order attribute (for experiments)
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47033
tuning -- don't refer to old, internal version number (needlessly confusing now)
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47032
more weight attribute tuning
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47031
use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47030
internal renamings
blanchet [Tue, 20 Mar 2012 00:44:30 +0100] rev 47029
renamed E weight attribute
wenzelm [Mon, 19 Mar 2012 23:17:18 +0100] rev 47028
tuned proofs;
wenzelm [Mon, 19 Mar 2012 23:08:27 +0100] rev 47027
explicit propagation of assignment event, even if changed command set is empty;
discontinued slightly odd Document_View.update_snapshot/flush_snapshot;
wenzelm [Mon, 19 Mar 2012 21:52:09 +0100] rev 47026
modernized axiomatizations;
wenzelm [Mon, 19 Mar 2012 21:49:52 +0100] rev 47025
modernized axiomatizations;
tuned proofs;
wenzelm [Mon, 19 Mar 2012 21:25:15 +0100] rev 47024
updated Misc_Legacy.freeze_thaw;
wenzelm [Mon, 19 Mar 2012 21:16:19 +0100] rev 47023
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
wenzelm [Mon, 19 Mar 2012 21:10:33 +0100] rev 47022
moved some legacy stuff;
wenzelm [Mon, 19 Mar 2012 20:32:57 +0100] rev 47021
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm [Mon, 19 Mar 2012 19:49:54 +0100] rev 47020
merged
paulson [Mon, 19 Mar 2012 15:20:00 +0000] rev 47019
merged
paulson [Mon, 19 Mar 2012 15:19:38 +0000] rev 47018
More structured proofs for cardinalities
paulson [Mon, 19 Mar 2012 10:52:48 +0000] rev 47017
merged
paulson [Fri, 16 Mar 2012 17:41:53 +0000] rev 47016
more structured case and induction proofs
blanchet [Mon, 19 Mar 2012 12:43:46 +0100] rev 47015
better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete
wenzelm [Mon, 19 Mar 2012 18:18:42 +0100] rev 47014
allow keyword tags to be redefined, but not the command category;
wenzelm [Mon, 19 Mar 2012 15:56:27 +0100] rev 47013
further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;
wenzelm [Mon, 19 Mar 2012 14:59:31 +0100] rev 47012
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm [Sun, 18 Mar 2012 22:09:00 +0100] rev 47011
more robust bash interpolation;
wenzelm [Sun, 18 Mar 2012 22:06:37 +0100] rev 47010
more ambitious scalac options for makedist;
wenzelm [Sun, 18 Mar 2012 21:52:50 +0100] rev 47009
less noisy Isabelle/Scala build process;
wenzelm [Sun, 18 Mar 2012 13:59:54 +0100] rev 47008
comment;
wenzelm [Sun, 18 Mar 2012 13:51:51 +0100] rev 47007
tuned;
wenzelm [Sun, 18 Mar 2012 13:37:11 +0100] rev 47006
tuned;
wenzelm [Sun, 18 Mar 2012 13:04:22 +0100] rev 47005
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;
wenzelm [Sun, 18 Mar 2012 12:51:44 +0100] rev 47004
tuned;
wenzelm [Sun, 18 Mar 2012 10:28:31 +0100] rev 47003
tuned structure;
haftmann [Sun, 18 Mar 2012 08:57:45 +0100] rev 47002
comments for uniformity
wenzelm [Sat, 17 Mar 2012 23:55:03 +0100] rev 47001
proper naming of simprocs according to actual target context;
afford pervasive declaration which makes results available with qualified name from outside;
wenzelm [Sat, 17 Mar 2012 23:50:47 +0100] rev 47000
amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
wenzelm [Sat, 17 Mar 2012 22:46:19 +0100] rev 46999
more precise syntax;
wenzelm [Sat, 17 Mar 2012 17:58:40 +0100] rev 46998
more antiquotations;
wenzelm [Sat, 17 Mar 2012 17:44:29 +0100] rev 46997
misc tuning to accomodate scala-2.10.0-M2;
wenzelm [Sat, 17 Mar 2012 17:36:10 +0100] rev 46996
include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions;
wenzelm [Sat, 17 Mar 2012 16:13:41 +0100] rev 46995
merged
paulson [Sat, 17 Mar 2012 12:37:32 +0000] rev 46994
merged
paulson [Sat, 17 Mar 2012 12:36:11 +0000] rev 46993
tidying and structured proofs
wenzelm [Sat, 17 Mar 2012 16:07:03 +0100] rev 46992
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
actually make "raw_def" internal (cf. 80123a220219);
wenzelm [Sat, 17 Mar 2012 15:33:08 +0100] rev 46991
tuned proofs;
wenzelm [Sat, 17 Mar 2012 14:01:09 +0100] rev 46990
simultaneous read_fields -- e.g. relevant for sort assignment;
wenzelm [Sat, 17 Mar 2012 13:06:23 +0100] rev 46989
added Syntax.read_typs;
tuned parallelism for syntax operations;
wenzelm [Sat, 17 Mar 2012 12:52:40 +0100] rev 46988
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm [Sat, 17 Mar 2012 12:26:19 +0100] rev 46987
tuned message;
wenzelm [Sat, 17 Mar 2012 12:21:15 +0100] rev 46986
tuned proofs;
wenzelm [Sat, 17 Mar 2012 12:00:11 +0100] rev 46985
tuned proofs;
wenzelm [Sat, 17 Mar 2012 11:59:59 +0100] rev 46984
tuned exception;
wenzelm [Sat, 17 Mar 2012 11:57:03 +0100] rev 46983
merged;
haftmann [Sat, 17 Mar 2012 11:35:18 +0100] rev 46982
spelt out missing colemmas
haftmann [Sat, 17 Mar 2012 08:00:18 +0100] rev 46981
generalized INF_INT_eq, SUP_UN_eq
haftmann [Fri, 16 Mar 2012 22:26:55 +0100] rev 46980
tuned specifications
wenzelm [Sat, 17 Mar 2012 11:23:14 +0100] rev 46979
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
tuned;
wenzelm [Sat, 17 Mar 2012 10:55:08 +0100] rev 46978
tuned grouping -- merely indicate order of magnitude;
wenzelm [Sat, 17 Mar 2012 10:54:15 +0100] rev 46977
slightly more parallel find_theorems;
wenzelm [Sat, 17 Mar 2012 09:51:18 +0100] rev 46976
'definition' no longer exports the foundational "raw_def";
wenzelm [Sat, 17 Mar 2012 00:17:30 +0100] rev 46975
some attempts to fit source on screen;
wenzelm [Fri, 16 Mar 2012 22:48:38 +0100] rev 46974
eliminated odd 'finalconsts' / Theory.add_finals;
wenzelm [Fri, 16 Mar 2012 22:31:19 +0100] rev 46973
modernized axiomatization;
eliminated odd 'finalconsts';
wenzelm [Fri, 16 Mar 2012 22:22:05 +0100] rev 46972
modernized axiomatization;
eliminated odd 'finalconsts';
wenzelm [Fri, 16 Mar 2012 21:59:19 +0100] rev 46971
afford strict Args.type_name (cf. 29e88714ffe4);
wenzelm [Fri, 16 Mar 2012 21:40:21 +0100] rev 46970
check declared vs. defined commands at end of session;
wenzelm [Fri, 16 Mar 2012 21:20:23 +0100] rev 46969
more abstract heading level;
wenzelm [Fri, 16 Mar 2012 20:45:47 +0100] rev 46968
less redundant data;
wenzelm [Fri, 16 Mar 2012 20:33:33 +0100] rev 46967
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
discontinued obsolete Keyword.thy_switch;
wenzelm [Fri, 16 Mar 2012 18:21:22 +0100] rev 46966
merged
paulson [Fri, 16 Mar 2012 16:32:34 +0000] rev 46965
ZF news
paulson [Fri, 16 Mar 2012 16:29:51 +0000] rev 46964
merged
paulson [Fri, 16 Mar 2012 16:29:28 +0000] rev 46963
Structured transfinite induction proofs
huffman [Fri, 16 Mar 2012 15:51:53 +0100] rev 46962
make more word theorems respect int/bin distinction
wenzelm [Fri, 16 Mar 2012 18:20:12 +0100] rev 46961
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm [Fri, 16 Mar 2012 14:46:13 +0100] rev 46960
refute_params are given in *this* theory;
wenzelm [Fri, 16 Mar 2012 14:42:11 +0100] rev 46959
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm [Fri, 16 Mar 2012 13:05:30 +0100] rev 46958
define keywords early when processing the theory header, before running the body commands;
wenzelm [Fri, 16 Mar 2012 11:26:55 +0100] rev 46957
clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;
wenzelm [Thu, 15 Mar 2012 23:06:22 +0100] rev 46956
Isabelle/jEdit supports user-defined Isar commands within the running session;
wenzelm [Thu, 15 Mar 2012 22:21:28 +0100] rev 46955
merged
paulson [Thu, 15 Mar 2012 17:38:05 +0000] rev 46954
beautification and structured proofs
paulson [Thu, 15 Mar 2012 16:35:02 +0000] rev 46953
replacing ":" by "\<in>"
paulson [Thu, 15 Mar 2012 15:54:22 +0000] rev 46952
Rewrote some induction proofs to be structured
wenzelm [Thu, 15 Mar 2012 22:20:07 +0100] rev 46951
more precise TPTP keywords and dependencies;
wenzelm [Thu, 15 Mar 2012 22:08:53 +0100] rev 46950
declare command keywords via theory header, including strict checking outside Pure;
wenzelm [Thu, 15 Mar 2012 20:07:00 +0100] rev 46949
prefer formally checked @{keyword} parser;
wenzelm [Thu, 15 Mar 2012 19:48:19 +0100] rev 46948
added ML antiquotation @{keyword};
wenzelm [Thu, 15 Mar 2012 19:02:34 +0100] rev 46947
declare minor keywords via theory header;
wenzelm [Thu, 15 Mar 2012 17:45:54 +0100] rev 46946
more explicit header_edits before main text_edits;
handle reparses caused by syntax update;
wenzelm [Thu, 15 Mar 2012 17:40:26 +0100] rev 46945
declare keywords as side-effect of header edit;
parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);
wenzelm [Thu, 15 Mar 2012 14:39:42 +0100] rev 46944
more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm [Thu, 15 Mar 2012 14:22:54 +0100] rev 46943
clarified syntax of prospective keywords;
wenzelm [Thu, 15 Mar 2012 14:13:49 +0100] rev 46942
basic support for outer syntax keywords in theory header;
wenzelm [Thu, 15 Mar 2012 11:37:56 +0100] rev 46941
maintain Version.syntax within document state;
clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;
wenzelm [Thu, 15 Mar 2012 10:16:21 +0100] rev 46940
explicit Outer_Syntax.Decl;