| Fri, 06 Mar 2009 15:31:07 +0100 |
blanchet |
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
|
changeset |
files
|
| Fri, 06 Mar 2009 15:51:18 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 06 Mar 2009 11:10:57 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 06 Mar 2009 11:10:18 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
changeset |
files
|
| Thu, 05 Mar 2009 08:24:28 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
changeset |
files
|
| Thu, 05 Mar 2009 08:23:10 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 05 Mar 2009 08:23:09 +0100 |
haftmann |
moved complete_lattice to Set.thy
|
changeset |
files
|
| Thu, 05 Mar 2009 08:23:08 +0100 |
haftmann |
dropped Id
|
changeset |
files
|
| Fri, 06 Mar 2009 14:51:18 +0100 |
haftmann |
corrected slip in NEWS
|
changeset |
files
|
| Fri, 06 Mar 2009 14:33:42 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 06 Mar 2009 14:33:19 +0100 |
haftmann |
added strict_mono predicate
|
changeset |
files
|
| Fri, 06 Mar 2009 11:50:32 +0100 |
wenzelm |
Identifiers of some old CVS file versions;
|
changeset |
files
|
| Fri, 06 Mar 2009 11:28:07 +0100 |
wenzelm |
recovered generated files;
|
changeset |
files
|
| Fri, 06 Mar 2009 11:25:54 +0100 |
wenzelm |
more precise deps;
|
changeset |
files
|
| Fri, 06 Mar 2009 09:35:43 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 06 Mar 2009 09:35:29 +0100 |
nipkow |
Added Docs
|
changeset |
files
|
| Thu, 05 Mar 2009 23:12:59 +0100 |
wenzelm |
render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
|
changeset |
files
|
| Thu, 05 Mar 2009 21:06:59 +0100 |
wenzelm |
removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
|
changeset |
files
|
| Thu, 05 Mar 2009 20:55:28 +0100 |
wenzelm |
removed unused TableFun().fold_map and GraphFun().fold_map_nodes;
|
changeset |
files
|
| Thu, 05 Mar 2009 20:17:02 +0100 |
wenzelm |
removed spurious occurrences of old rep_ss;
|
changeset |
files
|
| Thu, 05 Mar 2009 19:48:02 +0100 |
wenzelm |
Thm.add_oracle interface: replaced old bstring by binding;
|
changeset |
files
|
| Thu, 05 Mar 2009 18:19:20 +0100 |
wenzelm |
silent chmod;
|
changeset |
files
|
| Thu, 05 Mar 2009 17:35:37 +0100 |
wenzelm |
Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
|
changeset |
files
|
| Thu, 05 Mar 2009 17:09:07 +0100 |
wenzelm |
close_schematic_term: uniform order of types/terms;
|
changeset |
files
|
| Thu, 05 Mar 2009 15:27:07 +0100 |
wenzelm |
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
|
changeset |
files
|
| Thu, 05 Mar 2009 15:25:35 +0100 |
wenzelm |
TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
|
changeset |
files
|
| Thu, 05 Mar 2009 14:29:02 +0100 |
wenzelm |
fixed proofs -- follow-up to ecd6f0ca62ea;
|
changeset |
files
|
| Thu, 05 Mar 2009 12:11:25 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name");
|
changeset |
files
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
changeset |
files
|
| Thu, 05 Mar 2009 11:58:53 +0100 |
wenzelm |
eliminated obsolete ProofContext.full_bname;
|
changeset |
files
|
| Thu, 05 Mar 2009 10:54:03 +0100 |
wenzelm |
Binding.prefix_of;
|
changeset |
files
|
| Thu, 05 Mar 2009 10:53:49 +0100 |
wenzelm |
adapted Binding.dest;
|
changeset |
files
|
| Thu, 05 Mar 2009 10:52:07 +0100 |
wenzelm |
added prefix_of;
|
changeset |
files
|
| Thu, 05 Mar 2009 10:19:51 +0100 |
blanchet |
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
|
changeset |
files
|
| Thu, 05 Mar 2009 02:32:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 17:12:23 -0800 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
changeset |
files
|
| Thu, 05 Mar 2009 02:27:54 +0100 |
wenzelm |
regenerated document;
|
changeset |
files
|
| Thu, 05 Mar 2009 02:24:36 +0100 |
wenzelm |
merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
|
changeset |
files
|
| Thu, 05 Mar 2009 02:20:06 +0100 |
wenzelm |
dummy changes to produce a new changeset of these files;
|
changeset |
files
|
| Thu, 05 Mar 2009 01:55:38 +0100 |
wenzelm |
updated generated file -- changed since @{ML} now ignores source flag;
|
changeset |
files
|
| Thu, 05 Mar 2009 00:16:28 +0100 |
wenzelm |
fixed document;
|
changeset |
files
|
| Wed, 04 Mar 2009 23:52:47 +0100 |
wenzelm |
removed old/broken CVS Ids;
|
changeset |
files
|
| Wed, 04 Mar 2009 23:05:32 +0100 |
wenzelm |
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
|
changeset |
files
|
| Wed, 04 Mar 2009 19:22:32 +0000 |
chaieb |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 19:21:56 +0000 |
chaieb |
Moved general theorems about sums and products to FiniteSet.thy
|
changeset |
files
|
| Wed, 04 Mar 2009 19:21:56 +0000 |
chaieb |
fixed proofs; added rules as default simp-rules
|
changeset |
files
|
| Wed, 04 Mar 2009 19:21:56 +0000 |
chaieb |
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
|
changeset |
files
|
| Wed, 04 Mar 2009 19:21:55 +0000 |
chaieb |
Added Libray dependency on Topology_Euclidean_Space
|
changeset |
files
|
| Wed, 04 Mar 2009 19:21:55 +0000 |
chaieb |
Added general theorems for fold_image, setsum and set_prod
|
changeset |
files
|
| Wed, 04 Mar 2009 19:21:28 +0000 |
chaieb |
fixed proofs
|
changeset |
files
|
| Wed, 04 Mar 2009 10:54:47 +0000 |
chaieb |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 10:33:14 +0000 |
chaieb |
merged
|
changeset |
files
|
| Wed, 25 Feb 2009 10:29:01 +0000 |
chaieb |
merged
|
changeset |
files
|
| Wed, 25 Feb 2009 10:28:49 +0000 |
chaieb |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 18:18:05 +0100 |
blanchet |
Second try at adding "nitpick_const_def" attribute.
|
changeset |
files
|
| Wed, 04 Mar 2009 15:49:39 +0100 |
blanchet |
Fix parentheses.
|
changeset |
files
|
| Wed, 04 Mar 2009 15:33:07 +0100 |
blanchet |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 15:32:57 +0100 |
blanchet |
Added "nitpick_const_simp" attribute to Nominal primrec.
|
changeset |
files
|
| Wed, 04 Mar 2009 14:23:54 +0100 |
wenzelm |
NEWS: renamed o2s to Option.set;
|
changeset |
files
|
| Wed, 04 Mar 2009 13:42:23 +0100 |
haftmann |
less arbitrary occurrences of undefined
|
changeset |
files
|
| Wed, 04 Mar 2009 13:41:59 +0100 |
haftmann |
datatype antiquotation does not assume LaTeX as output any longer
|
changeset |
files
|
| Wed, 04 Mar 2009 11:49:12 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 11:48:52 +0100 |
nipkow |
Option.thy
|
changeset |
files
|
| Wed, 04 Mar 2009 11:44:05 +0100 |
haftmann |
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
|
changeset |
files
|
| Wed, 04 Mar 2009 11:37:50 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 10:52:47 +0100 |
haftmann |
explicit error message for `improper` instances lacking explicit instance parameter constants
|
changeset |
files
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
changeset |
files
|
| Wed, 04 Mar 2009 11:05:02 +0100 |
blanchet |
Merge.
|
changeset |
files
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
changeset |
files
|
| Wed, 04 Mar 2009 10:43:39 +0100 |
blanchet |
Made Refute.norm_rhs public, so I can use it in Nitpick.
|
changeset |
files
|
| Sun, 01 Mar 2009 18:40:16 +0100 |
blanchet |
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
|
changeset |
files
|
| Tue, 24 Feb 2009 16:12:27 +0100 |
blanchet |
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
|
changeset |
files
|
| Wed, 04 Mar 2009 10:47:35 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
changeset |
files
|
| Wed, 04 Mar 2009 00:05:20 +0100 |
wenzelm |
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
|
changeset |
files
|
| Tue, 03 Mar 2009 21:53:52 +0100 |
wenzelm |
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
|
changeset |
files
|
| Tue, 03 Mar 2009 21:49:34 +0100 |
wenzelm |
tuned str_of, now subject to verbose flag;
|
changeset |
files
|
| Tue, 03 Mar 2009 21:49:05 +0100 |
wenzelm |
added @{binding} ML antiquotations;
|
changeset |
files
|
| Tue, 03 Mar 2009 21:48:40 +0100 |
wenzelm |
added print_properties, print_position (again);
|
changeset |
files
|
| Tue, 03 Mar 2009 19:30:43 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 19:21:10 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 13:20:53 +0100 |
haftmann |
tuned manuals
|
changeset |
files
|
| Tue, 03 Mar 2009 11:00:51 +0100 |
haftmann |
more canonical directory structure of manuals
|
changeset |
files
|
| Tue, 03 Mar 2009 18:33:21 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
changeset |
files
|
| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
changeset |
files
|
| Tue, 03 Mar 2009 18:31:59 +0100 |
wenzelm |
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
|
changeset |
files
|
| Tue, 03 Mar 2009 17:42:30 +0100 |
wenzelm |
added markup for binding;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:12:52 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:09 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:08 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:07 +0100 |
wenzelm |
renamed Binding.display to Binding.str_of, which is slightly more canonical;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:54:12 +0100 |
wenzelm |
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:53:29 +0100 |
wenzelm |
moved name space externalization flags back to name_space.ML;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:52:13 +0100 |
wenzelm |
moved name space externalization flags back to name_space.ML;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:16:05 +0100 |
wenzelm |
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
|
changeset |
files
|
| Tue, 03 Mar 2009 14:08:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
changeset |
files
|
| Tue, 03 Mar 2009 14:07:23 +0100 |
wenzelm |
added type binding and val empty_binding;
|
changeset |
files
|
| Tue, 03 Mar 2009 13:22:01 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Tue, 03 Mar 2009 12:12:38 +0100 |
wenzelm |
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
|
changeset |
files
|
| Tue, 03 Mar 2009 12:14:52 +1100 |
Timothy Bourke |
Implement Makarius's suggestion for improved type pattern parsing.
|
changeset |
files
|
| Mon, 02 Mar 2009 18:11:39 +1100 |
Timothy Bourke |
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
|
changeset |
files
|
| Mon, 02 Mar 2009 20:31:27 +0100 |
wenzelm |
adapted to lates experimental version;
|
changeset |
files
|
| Mon, 02 Mar 2009 20:29:43 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Mon, 02 Mar 2009 18:50:41 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 02 Mar 2009 16:58:39 +0100 |
haftmann |
reduced confusion code_funcgr vs. code_wellsorted
|
changeset |
files
|
| Mon, 02 Mar 2009 16:58:39 +0100 |
haftmann |
better markup
|
changeset |
files
|
| Mon, 02 Mar 2009 17:26:23 +0100 |
nipkow |
name fix
|
changeset |
files
|
| Mon, 02 Mar 2009 16:54:13 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
changeset |
files
|
| Mon, 02 Mar 2009 12:34:03 +0000 |
chaieb |
Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Mon, 02 Mar 2009 12:33:12 +0000 |
chaieb |
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
|
changeset |
files
|
| Mon, 02 Mar 2009 10:55:54 +0100 |
wenzelm |
fixed broken @{file} refs;
|
changeset |
files
|
| Mon, 02 Mar 2009 10:48:22 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 02 Mar 2009 08:26:03 +0100 |
haftmann |
using plain ISABELLE_PROCESS
|
changeset |
files
|
| Mon, 02 Mar 2009 08:15:54 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 02 Mar 2009 08:15:32 +0100 |
haftmann |
ignore ISABELLE_LINE_EDITOR for code generation
|
changeset |
files
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
changeset |
files
|