| Fri, 30 Jan 2009 12:48:57 +0000 |
chaieb |
Added real related theorems from Fact.thy
|
changeset |
files
|
| Fri, 30 Jan 2009 12:48:56 +0000 |
chaieb |
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
|
changeset |
files
|
| Fri, 30 Jan 2009 12:48:56 +0000 |
chaieb |
moved upwards in thy graph, real related theorems moved to Transcendental.thy
|
changeset |
files
|
| Thu, 29 Jan 2009 22:29:44 +0100 |
berghofe |
Enclosed name containing _'s in @{text ...} antiquotation to make document
|
changeset |
files
|
| Thu, 29 Jan 2009 22:28:03 +0100 |
berghofe |
Added strong congruence rule for UN.
|
changeset |
files
|
| Thu, 29 Jan 2009 22:27:07 +0100 |
berghofe |
Added abs_def attribute.
|
changeset |
files
|
| Thu, 29 Jan 2009 15:29:41 +0000 |
chaieb |
removed definition of funpow , reusing that of Relation_Power
|
changeset |
files
|
| Thu, 29 Jan 2009 14:56:29 +0000 |
chaieb |
Added Formal_Power_Series in imports
|
changeset |
files
|
| Thu, 29 Jan 2009 14:56:29 +0000 |
chaieb |
A formalization of formal power series
|
changeset |
files
|
| Thu, 29 Jan 2009 14:56:28 +0000 |
chaieb |
Inserted Formal_Power_Series.thy under Library
|
changeset |
files
|
| Thu, 29 Jan 2009 12:24:00 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Thu, 29 Jan 2009 12:05:19 +0000 |
paulson |
Minor reorganisation of the Skolemization code
|
changeset |
files
|
| Tue, 13 Jan 2009 16:47:24 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Fri, 09 Jan 2009 15:54:41 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Fri, 19 Dec 2008 11:49:08 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Mon, 15 Dec 2008 10:40:52 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Thu, 11 Dec 2008 14:50:02 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Wed, 10 Dec 2008 15:38:00 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Wed, 10 Dec 2008 12:17:02 +0000 |
paulson |
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Fri, 05 Dec 2008 15:52:12 +0000 |
paulson |
Updated comments.
|
changeset |
files
|
| Thu, 29 Jan 2009 09:35:51 +0000 |
chaieb |
dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
|
changeset |
files
|
| Wed, 28 Jan 2009 13:23:59 +0000 |
chaieb |
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
|
changeset |
files
|
| Thu, 29 Jan 2009 10:08:25 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 29 Jan 2009 10:07:43 +0100 |
nipkow |
commented out unused lemmas. May need to be put back by Brian.
|
changeset |
files
|
| Wed, 28 Jan 2009 21:49:25 +0100 |
nipkow |
-
|
changeset |
files
|
| Wed, 28 Jan 2009 17:12:25 +0100 |
nipkow |
removed spurious conflic msg
|
changeset |
files
|
| Wed, 28 Jan 2009 16:57:36 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
changeset |
files
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
changeset |
files
|
| Wed, 28 Jan 2009 16:35:57 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 16:35:42 +0100 |
haftmann |
explicit check for exactly one type variable in class specification elements
|
changeset |
files
|
| Wed, 28 Jan 2009 06:03:46 -0800 |
huffman |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 22:39:41 -0800 |
huffman |
merged
|
changeset |
files
|
| Thu, 22 Jan 2009 06:42:05 -0800 |
huffman |
removed use of prev_cont_thms reference
|
changeset |
files
|
| Thu, 22 Jan 2009 06:09:41 -0800 |
huffman |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 21:01:15 -0800 |
huffman |
add lemmas about div/mod with multiplication
|
changeset |
files
|
| Wed, 21 Jan 2009 20:20:56 -0800 |
huffman |
add lemmas about smult
|
changeset |
files
|
| Wed, 28 Jan 2009 13:36:24 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 13:36:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
changeset |
files
|
| Wed, 28 Jan 2009 11:04:45 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 11:03:42 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
changeset |
files
|
| Wed, 28 Jan 2009 11:03:16 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
changeset |
files
|
| Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
added lemma abs_sng
|
changeset |
files
|
| Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
nat is a bot instance
|
changeset |
files
|
| Wed, 28 Jan 2009 11:02:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
changeset |
files
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
changeset |
files
|
| Wed, 28 Jan 2009 11:36:45 +0100 |
wenzelm |
more robust treatment of SwingUtilities.isEventDispatchThread;
|
changeset |
files
|
| Wed, 28 Jan 2009 10:43:31 +0100 |
wenzelm |
annotate shared vars as @volatile;
|
changeset |
files
|
| Tue, 27 Jan 2009 19:56:26 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 27 Jan 2009 19:56:20 +0100 |
wenzelm |
added label;
|
changeset |
files
|
| Tue, 27 Jan 2009 15:47:22 +0100 |
wenzelm |
plain non-dependent types;
|
changeset |
files
|
| Tue, 27 Jan 2009 15:22:46 +0100 |
wenzelm |
turned IsarDocument into trait for IsabelleProcess;
|
changeset |
files
|
| Tue, 27 Jan 2009 14:45:52 +0100 |
wenzelm |
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
|
changeset |
files
|
| Tue, 27 Jan 2009 14:28:51 +0100 |
wenzelm |
thm_proof: recovered single-threaded version;
|
changeset |
files
|
| Tue, 27 Jan 2009 13:52:32 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 13:41:45 +0100 |
wenzelm |
recovered example types from WordMain.thy;
|
changeset |
files
|
| Tue, 27 Jan 2009 12:59:38 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 12:59:22 +0100 |
wenzelm |
added share_common_data -- reduces heap space, but takes long;
|
changeset |
files
|
| Tue, 27 Jan 2009 12:57:24 +0100 |
wenzelm |
use https;
|
changeset |
files
|
| Tue, 27 Jan 2009 00:42:12 +0100 |
wenzelm |
thm_proof: replaced lazy by composed futures;
|
changeset |
files
|
| Tue, 27 Jan 2009 00:29:37 +0100 |
wenzelm |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
changeset |
files
|
| Mon, 26 Jan 2009 22:15:35 +0100 |
haftmann |
explicit constraints
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:51 +0100 |
haftmann |
entry point for Word library now named Word
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:19 +0100 |
haftmann |
fixed reading of class specs: declare class operations in context
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:18 +0100 |
haftmann |
stripped Id
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
streamlined definitions, executable equality
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
tuned header
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:16 +0100 |
haftmann |
entry point for Word library now named Word
|
changeset |
files
|
| Mon, 26 Jan 2009 08:23:55 +0100 |
haftmann |
correct proof of assm_intro rule
|
changeset |
files
|
| Mon, 26 Jan 2009 08:23:41 +0100 |
haftmann |
sorted_take, sorted_drop
|
changeset |
files
|
| Fri, 23 Jan 2009 19:52:02 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 23 Jan 2009 19:51:49 +0100 |
haftmann |
fixed fixme
|
changeset |
files
|
| Fri, 23 Jan 2009 19:51:49 +0100 |
haftmann |
avoiding misleading name duplicate
|
changeset |
files
|
| Fri, 23 Jan 2009 19:51:48 +0100 |
haftmann |
lemmas dom_const, dom_if
|
changeset |
files
|
| Fri, 23 Jan 2009 15:37:12 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 23 Jan 2009 09:06:14 +0100 |
immler |
moved all output to watcher-thread
|
changeset |
files
|
| Fri, 23 Jan 2009 10:21:48 +0100 |
haftmann |
be more liberal with selected code statements
|
changeset |
files
|
| Fri, 23 Jan 2009 10:21:27 +0100 |
haftmann |
making SMLNJ happy
|
changeset |
files
|
| Thu, 22 Jan 2009 11:23:15 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 22 Jan 2009 09:08:58 +0100 |
haftmann |
binding replaces Binding.T
|
changeset |
files
|
| Thu, 22 Jan 2009 09:04:56 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
| Thu, 22 Jan 2009 09:04:46 +0100 |
haftmann |
simplified handling of base sort, dropped axclass
|
changeset |
files
|
| Thu, 22 Jan 2009 09:04:45 +0100 |
haftmann |
dropped print_interps
|
changeset |
files
|
| Thu, 22 Jan 2009 09:04:45 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
| Wed, 21 Jan 2009 23:42:37 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
allow empty class specs
|
changeset |
files
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
changeset |
files
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
changeset |
files
|
| Wed, 21 Jan 2009 23:25:17 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
changeset |
files
|
| Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
changeset |
files
|
| Wed, 21 Jan 2009 22:26:48 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
changeset |
files
|
| Wed, 21 Jan 2009 20:24:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 20:20:43 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Wed, 21 Jan 2009 20:05:31 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 15:26:02 +0100 |
immler |
removed vampire-wrapper (remote-script covers that)
|
changeset |
files
|
| Wed, 21 Jan 2009 15:22:51 +0100 |
immler |
2 provers
|
changeset |
files
|
| Wed, 21 Jan 2009 14:57:33 +0100 |
immler |
tuned;
|
changeset |
files
|
| Tue, 20 Jan 2009 23:35:37 +0100 |
immler |
do not interrupt successful thread
|
changeset |
files
|
| Tue, 20 Jan 2009 22:19:46 +0100 |
immler |
cancel whole group
|
changeset |
files
|
| Tue, 20 Jan 2009 20:58:25 +0100 |
immler |
Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip
|
changeset |
files
|
| Tue, 20 Jan 2009 20:58:08 +0100 |
immler |
pass timeout to prover;
|
changeset |
files
|
| Tue, 20 Jan 2009 18:12:06 +0100 |
immler |
typo
|
changeset |
files
|
| Tue, 20 Jan 2009 18:10:25 +0100 |
immler |
merged
|
changeset |
files
|
| Tue, 20 Jan 2009 16:05:57 +0100 |
immler |
modified remote script;
|
changeset |
files
|
| Mon, 19 Jan 2009 20:24:10 +0100 |
immler |
Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip
|
changeset |
files
|
| Wed, 14 Jan 2009 20:19:47 +0100 |
immler |
removed useless
|
changeset |
files
|
| Mon, 12 Jan 2009 16:16:05 +0100 |
immler |
simplified usage of remote-script; added compatible remote-atps
|
changeset |
files
|
| Wed, 21 Jan 2009 18:37:44 +0100 |
haftmann |
dropped print_interps
|
changeset |
files
|
| Wed, 21 Jan 2009 18:27:43 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
| Wed, 21 Jan 2009 16:51:45 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 16:50:09 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 16:48:15 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
refined witness algebra
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
code cleanup
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
wrecked old locale package and related modules
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:02 +0100 |
haftmann |
improved and corrected reading of class specs -- still draft version
|
changeset |
files
|
| Wed, 21 Jan 2009 16:47:01 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 20 Jan 2009 19:09:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Jan 2009 18:08:31 +0100 |
wenzelm |
replaced java.util.Properties by plain association list;
|
changeset |
files
|
| Tue, 20 Jan 2009 18:06:56 +0100 |
wenzelm |
replaced java.util.Properties by plain association list;
|
changeset |
files
|
| Tue, 20 Jan 2009 18:05:21 +0100 |
wenzelm |
IsabelleSystem: provide Symbol.Interpretation;
|
changeset |
files
|
| Tue, 20 Jan 2009 18:04:37 +0100 |
wenzelm |
more general init of Symbol.Interpretation, independent of IsabelleSystem instance;
|
changeset |
files
|
| Mon, 19 Jan 2009 23:40:29 +0100 |
wenzelm |
more robust handling of quick_and_dirty;
|
changeset |
files
|
| Mon, 19 Jan 2009 21:20:18 +0100 |
ballarin |
Merged, overriding earlier fix.
|
changeset |
files
|
| Mon, 19 Jan 2009 20:37:08 +0100 |
ballarin |
Fixed tutorial to compile with new locales; grammar of new locale commands.
|
changeset |
files
|
| Mon, 19 Jan 2009 20:05:41 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Mon, 19 Jan 2009 19:38:03 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Mon, 19 Jan 2009 16:03:04 +0100 |
wenzelm |
intern names of elements and attributes;
|
changeset |
files
|
| Mon, 19 Jan 2009 13:38:59 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 19 Jan 2009 13:38:23 +0100 |
haftmann |
lcp = paulson
|
changeset |
files
|
| Mon, 19 Jan 2009 13:37:24 +0100 |
haftmann |
"code equation" replaces "defining equation"
|
changeset |
files
|
| Mon, 19 Jan 2009 08:16:43 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 19 Jan 2009 08:16:42 +0100 |
haftmann |
improved tackling of subclasses
|
changeset |
files
|
| Mon, 19 Jan 2009 08:16:42 +0100 |
haftmann |
tuned proof
|
changeset |
files
|
| Sun, 18 Jan 2009 21:40:53 +0100 |
haftmann |
smart path detection
|
changeset |
files
|
| Sun, 18 Jan 2009 21:36:59 +0100 |
haftmann |
corrected user aliases
|
changeset |
files
|
| Sun, 18 Jan 2009 21:12:06 +0100 |
haftmann |
added churn script
|
changeset |
files
|
| Sun, 18 Jan 2009 20:06:51 +0100 |
wenzelm |
Scala wrapper for interactive Isar documents;
|
changeset |
files
|
| Sun, 18 Jan 2009 20:05:01 +0100 |
wenzelm |
added append_list, encode_list;
|
changeset |
files
|
| Sun, 18 Jan 2009 16:42:43 +0100 |
wenzelm |
join_results: when dependencies are resulved (but not finished yet),
|
changeset |
files
|
| Sun, 18 Jan 2009 16:33:09 +0100 |
wenzelm |
with_attributes: make double sure that unsafe attributes are avoided;
|
changeset |
files
|
| Sun, 18 Jan 2009 13:58:17 +0100 |
nipkow |
bug fixes
|
changeset |
files
|
| Sun, 18 Jan 2009 13:53:15 +0100 |
nipkow |
bug fixes
|
changeset |
files
|
| Sun, 18 Jan 2009 10:11:12 +0100 |
haftmann |
improved calculation of morphisms and rules
|
changeset |
files
|
| Sat, 17 Jan 2009 22:08:14 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sat, 17 Jan 2009 22:07:29 +0100 |
haftmann |
tuned signature
|
changeset |
files
|
| Sat, 17 Jan 2009 22:07:15 +0100 |
haftmann |
exported depedencies; tuned signature
|
changeset |
files
|
| Sat, 17 Jan 2009 10:40:03 -0800 |
huffman |
merged
|
changeset |
files
|
| Fri, 16 Jan 2009 13:07:44 -0800 |
huffman |
merged
|
changeset |
files
|
| Thu, 15 Jan 2009 14:33:38 -0800 |
huffman |
use match_tac instead of resolve_tac for continuity simproc
|
changeset |
files
|
| Thu, 15 Jan 2009 12:43:41 -0800 |
huffman |
more instance declarations for poly
|
changeset |
files
|
| Thu, 15 Jan 2009 12:43:12 -0800 |
huffman |
add lemmas about degree
|
changeset |
files
|
| Thu, 15 Jan 2009 10:00:31 -0800 |
huffman |
rename plength to psize
|
changeset |
files
|
| Thu, 15 Jan 2009 09:17:15 -0800 |
huffman |
rename divmod_poly to pdivmod
|
changeset |
files
|
| Thu, 15 Jan 2009 09:10:42 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 15 Jan 2009 08:11:50 -0800 |
huffman |
add strictness and compactness lemmas to Product_Cpo.thy
|
changeset |
files
|
| Wed, 14 Jan 2009 18:22:43 -0800 |
huffman |
rename Dsum.thy to Sum_Cpo.thy
|
changeset |
files
|
| Wed, 14 Jan 2009 18:18:48 -0800 |
huffman |
minimize dependencies
|
changeset |
files
|
| Wed, 14 Jan 2009 18:05:05 -0800 |
huffman |
add lemmas cont2monofunE, cont2cont_apply
|
changeset |
files
|
| Wed, 14 Jan 2009 17:12:21 -0800 |
huffman |
add Product_Cpo.thy
|
changeset |
files
|
| Wed, 14 Jan 2009 17:11:29 -0800 |
huffman |
change to simpler, more extensible continuity simproc
|
changeset |
files
|
| Sat, 17 Jan 2009 12:38:50 +0100 |
nipkow |
merged
|
changeset |
files
|
| Sat, 17 Jan 2009 12:38:05 +0100 |
nipkow |
bug fix
|
changeset |
files
|
| Sat, 17 Jan 2009 08:30:06 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sat, 17 Jan 2009 08:29:54 +0100 |
haftmann |
code cleanup
|
changeset |
files
|
| Sat, 17 Jan 2009 08:29:40 +0100 |
haftmann |
explicit equation morphism
|
changeset |
files
|
| Sat, 17 Jan 2009 08:29:19 +0100 |
haftmann |
close derivation of classrels
|
changeset |
files
|
| Sat, 17 Jan 2009 08:28:51 +0100 |
haftmann |
no document for HOL-Base
|
changeset |
files
|
| Fri, 16 Jan 2009 22:56:12 +0100 |
wenzelm |
moved message markup into Scala layer -- reduced redundancy;
|
changeset |
files
|
| Fri, 16 Jan 2009 22:54:11 +0100 |
wenzelm |
added parse_body_failsafe;
|
changeset |
files
|
| Fri, 16 Jan 2009 21:24:33 +0100 |
wenzelm |
define_state: use empty_state;
|
changeset |
files
|
| Fri, 16 Jan 2009 16:00:20 +0100 |
wenzelm |
provide end_document;
|
changeset |
files
|
| Fri, 16 Jan 2009 15:21:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 16 Jan 2009 15:21:26 +0100 |
wenzelm |
run command: check theory name for init;
|
changeset |
files
|
| Fri, 16 Jan 2009 15:20:31 +0100 |
wenzelm |
run_command: check theory name for init;
|
changeset |
files
|
| Fri, 16 Jan 2009 15:20:05 +0100 |
wenzelm |
export check_name;
|
changeset |
files
|
| Fri, 16 Jan 2009 15:19:10 +0100 |
haftmann |
fixed location of Imperative_HOL
|
changeset |
files
|
| Fri, 16 Jan 2009 15:14:16 +0100 |
haftmann |
adapted to changes in class package
|
changeset |
files
|
| Fri, 16 Jan 2009 14:59:06 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 16 Jan 2009 14:58:56 +0100 |
haftmann |
migrated class package to new locale implementation
|
changeset |
files
|
| Fri, 16 Jan 2009 14:58:12 +0100 |
haftmann |
corrected preparation of instances: parameters are proper names, not raw terms
|
changeset |
files
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
changeset |
files
|
| Fri, 16 Jan 2009 12:11:06 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 16 Jan 2009 12:10:51 +0100 |
wenzelm |
fold_entries: non-optional start, permissive;
|
changeset |
files
|
| Thu, 15 Jan 2009 17:22:38 +0100 |
wenzelm |
Result.toString: XML output of status messages;
|
changeset |
files
|
| Fri, 16 Jan 2009 08:29:11 +0100 |
haftmann |
added HOL-Base image
|
changeset |
files
|
| Fri, 16 Jan 2009 08:28:53 +0100 |
haftmann |
moved Univ_Poly to Library
|
changeset |
files
|
| Fri, 16 Jan 2009 08:05:03 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 16 Jan 2009 08:04:39 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 16 Jan 2009 08:04:38 +0100 |
haftmann |
added cert_read_declaration; more exports; tuned signature
|
changeset |
files
|
| Thu, 15 Jan 2009 15:51:50 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 15 Jan 2009 15:51:19 +0100 |
wenzelm |
command 'Isar.edit_document': actually invoke edit_document;
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:35 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:26 +0100 |
haftmann |
fixed error message spacing
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:25 +0100 |
haftmann |
tuned interpretation code
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:25 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:24 +0100 |
haftmann |
type constraints and sort intersection
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:24 +0100 |
haftmann |
dropped $Id$
|
changeset |
files
|
| Thu, 15 Jan 2009 14:52:23 +0100 |
haftmann |
decativate Toplevel.debug after reading
|
changeset |
files
|
| Thu, 15 Jan 2009 12:55:38 +0000 |
Christian Urban |
exported break reference
|
changeset |
files
|
| Thu, 15 Jan 2009 12:16:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 15 Jan 2009 11:55:22 +0100 |
wenzelm |
edit_document: proper edits/edit markup, including the document id;
|
changeset |
files
|
| Thu, 15 Jan 2009 11:53:49 +0100 |
wenzelm |
replaced command_state by edits/edit;
|
changeset |
files
|
| Thu, 15 Jan 2009 00:48:45 +0100 |
wenzelm |
removed junk;
|
changeset |
files
|
| Thu, 15 Jan 2009 00:44:19 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 14 Jan 2009 13:47:14 -0800 |
huffman |
one more [code del] declaration
|
changeset |
files
|
| Thu, 15 Jan 2009 00:44:06 +0100 |
wenzelm |
misc cleanup and simplification;
|
changeset |
files
|
| Thu, 15 Jan 2009 00:41:53 +0100 |
wenzelm |
added run_command (from isar_document.ML);
|
changeset |
files
|
| Thu, 15 Jan 2009 00:41:24 +0100 |
wenzelm |
added command_state markup;
|
changeset |
files
|
| Wed, 14 Jan 2009 19:38:55 +0100 |
wenzelm |
tuned ASCII art;
|
changeset |
files
|
| Tue, 13 Jan 2009 15:33:30 -0800 |
huffman |
declare pCons_0_0 [code post]
|
changeset |
files
|
| Tue, 13 Jan 2009 14:08:24 -0800 |
huffman |
merged
|
changeset |
files
|
| Tue, 13 Jan 2009 13:48:21 -0800 |
huffman |
code generation for polynomials
|
changeset |
files
|
| Tue, 13 Jan 2009 22:25:04 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 13 Jan 2009 13:02:16 -0800 |
huffman |
more [code del] declarations
|
changeset |
files
|
| Tue, 13 Jan 2009 10:18:23 -0800 |
huffman |
declare more definitions [code del]
|
changeset |
files
|
| Tue, 13 Jan 2009 08:58:56 -0800 |
huffman |
define polynomial multiplication using poly_rec
|
changeset |
files
|
| Tue, 13 Jan 2009 08:20:12 -0800 |
huffman |
merged.
|
changeset |
files
|
| Tue, 13 Jan 2009 08:19:14 -0800 |
huffman |
declare smult rules [simp]
|
changeset |
files
|
| Tue, 13 Jan 2009 07:40:05 -0800 |
huffman |
simplify proof of coeff_mult_degree_sum
|
changeset |
files
|
| Tue, 13 Jan 2009 06:57:08 -0800 |
huffman |
convert Deriv.thy to use new Polynomial library (incomplete)
|
changeset |
files
|
| Tue, 13 Jan 2009 06:55:13 -0800 |
huffman |
Integration imports ATP_Linkup (for metis)
|
changeset |
files
|
| Tue, 13 Jan 2009 22:20:49 +0100 |
wenzelm |
misc internal rearrangements;
|
changeset |
files
|
| Tue, 13 Jan 2009 17:34:12 +0100 |
wenzelm |
replaced sys_error by plain error;
|
changeset |
files
|
| Tue, 13 Jan 2009 14:31:02 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 12 Jan 2009 23:36:30 -0800 |
huffman |
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
|
changeset |
files
|
| Mon, 12 Jan 2009 22:41:08 -0800 |
huffman |
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
|
changeset |
files
|
| Mon, 12 Jan 2009 22:18:51 -0800 |
huffman |
add Polynomial.thy to makefile
|
changeset |
files
|
| Mon, 12 Jan 2009 22:16:35 -0800 |
huffman |
add lemmas poly_power, poly_roots_finite
|
changeset |
files
|
| Mon, 12 Jan 2009 12:10:41 -0800 |
huffman |
declare dvd_minus_iff and minus_dvd_iff [iff]
|
changeset |
files
|
| Mon, 12 Jan 2009 12:09:54 -0800 |
huffman |
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
|
changeset |
files
|
| Tue, 13 Jan 2009 13:47:35 +0100 |
wenzelm |
added Isar/isar_document.ML: Interactive Isar documents.
|
changeset |
files
|
| Tue, 13 Jan 2009 13:46:30 +0100 |
wenzelm |
export list;
|
changeset |
files
|
| Mon, 12 Jan 2009 10:09:23 -0800 |
huffman |
correctness and uniqueness of synthetic division
|
changeset |
files
|
| Mon, 12 Jan 2009 09:35:15 -0800 |
huffman |
add synthetic division algorithm for polynomials
|
changeset |
files
|
| Mon, 12 Jan 2009 09:04:25 -0800 |
huffman |
add list-style syntax for pCons
|
changeset |
files
|
| Mon, 12 Jan 2009 08:46:07 -0800 |
huffman |
add recursion combinator poly_rec; define poly function using poly_rec
|
changeset |
files
|
| Mon, 12 Jan 2009 08:15:07 -0800 |
huffman |
add lemmas degree_{add,diff}_less
|
changeset |
files
|
| Sun, 11 Jan 2009 21:50:05 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Jan 2009 12:05:50 -0800 |
huffman |
new theory of polynomials
|
changeset |
files
|
| Sun, 11 Jan 2009 21:49:59 +0100 |
wenzelm |
tuned categories;
|
changeset |
files
|
| Sun, 11 Jan 2009 20:40:09 +0100 |
wenzelm |
added outer_keyword.scala: Isar command keyword classification;
|
changeset |
files
|
| Sun, 11 Jan 2009 18:18:35 +0100 |
wenzelm |
added Goal.future_enabled abstraction -- now also checks that this is already
|
changeset |
files
|
| Sun, 11 Jan 2009 17:34:02 +0100 |
wenzelm |
load main entry points sequentially, for reduced memory demands;
|
changeset |
files
|
| Sun, 11 Jan 2009 16:56:59 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Jan 2009 14:23:54 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Jan 2009 16:41:48 +0100 |
wenzelm |
less ambitious ML_OPTIONS;
|
changeset |
files
|
| Sun, 11 Jan 2009 14:22:34 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Jan 2009 14:18:32 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sun, 11 Jan 2009 14:18:17 +0100 |
haftmann |
explicit bookkeeping of intro rules and axiom
|
changeset |
files
|
| Sun, 11 Jan 2009 14:18:16 +0100 |
haftmann |
stripped Id
|
changeset |
files
|
| Sun, 11 Jan 2009 14:18:16 +0100 |
haftmann |
construct explicit class morphism
|
changeset |
files
|
| Sun, 11 Jan 2009 13:48:11 +0100 |
wenzelm |
less ambitious ML_OPTIONS;
|
changeset |
files
|
| Sat, 10 Jan 2009 23:56:11 +0100 |
wenzelm |
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
|
changeset |
files
|
| Sat, 10 Jan 2009 21:47:02 +0100 |
wenzelm |
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
|
changeset |
files
|
| Sat, 10 Jan 2009 21:32:30 +0100 |
wenzelm |
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
|
changeset |
files
|
| Sat, 10 Jan 2009 16:58:56 +0100 |
wenzelm |
remove_thy: perform PureThy.cancel_proofs;
|
changeset |
files
|
| Sat, 10 Jan 2009 16:55:46 +0100 |
wenzelm |
added cancel_proofs, based on task groups of "entered" proofs;
|
changeset |
files
|
| Sat, 10 Jan 2009 16:54:55 +0100 |
wenzelm |
added pending_groups -- accumulates task groups of local derivations only;
|
changeset |
files
|
| Sat, 10 Jan 2009 16:53:12 +0100 |
wenzelm |
added cancel_group;
|
changeset |
files
|
| Sat, 10 Jan 2009 16:00:34 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Jan 2009 13:11:56 +0100 |
wenzelm |
schedule_futures: tuned final consolidation, explicit after_load phase;
|
changeset |
files
|
| Sat, 10 Jan 2009 13:10:38 +0100 |
wenzelm |
load_thy: explicit after_load phase for presentation;
|
changeset |
files
|
| Sat, 10 Jan 2009 13:10:07 +0100 |
wenzelm |
excursion: commit_exit internally -- checkpoints are fully persistent now;
|
changeset |
files
|
| Sat, 10 Jan 2009 15:55:19 +0100 |
wenzelm |
slightly more robust matching of session name;
|
changeset |
files
|
| Sat, 10 Jan 2009 01:28:31 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Jan 2009 01:06:32 +0100 |
wenzelm |
fixed proof involving dvd;
|
changeset |
files
|
| Sat, 10 Jan 2009 01:28:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 10 Jan 2009 01:28:03 +0100 |
wenzelm |
added force_result;
|
changeset |
files
|
| Sat, 10 Jan 2009 00:25:31 +0100 |
wenzelm |
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
|
changeset |
files
|
| Sat, 10 Jan 2009 00:24:07 +0100 |
wenzelm |
simplified join_proofs;
|
changeset |
files
|
| Fri, 09 Jan 2009 23:39:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jan 2009 23:34:36 +0100 |
wenzelm |
added split_thy_path;
|
changeset |
files
|
| Fri, 09 Jan 2009 23:33:59 +0100 |
wenzelm |
added running task markup;
|
changeset |
files
|
| Thu, 08 Jan 2009 13:18:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Jan 2009 12:15:23 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jan 2009 19:41:33 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jan 2009 09:49:01 -0800 |
huffman |
merged.
|
changeset |
files
|
| Fri, 09 Jan 2009 09:34:49 -0800 |
huffman |
fix proof broken by changes in dvd theory
|
changeset |
files
|
| Thu, 08 Jan 2009 21:13:40 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 08 Jan 2009 12:25:22 -0800 |
huffman |
remove type-specific proofs
|
changeset |
files
|
| Thu, 08 Jan 2009 10:43:09 -0800 |
huffman |
add lemma dvd_diff to class comm_ring_1
|
changeset |
files
|
| Thu, 08 Jan 2009 10:26:50 -0800 |
huffman |
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
|
changeset |
files
|
| Thu, 08 Jan 2009 10:07:39 -0800 |
huffman |
move lemmas mult_minus{left,right} inside class ring
|
changeset |
files
|
| Thu, 08 Jan 2009 09:58:36 -0800 |
huffman |
clean up division_ring proofs
|
changeset |
files
|
| Thu, 08 Jan 2009 09:12:29 -0800 |
huffman |
add class ring_div; generalize mod/diff/minus proofs for class ring_div
|
changeset |
files
|
| Thu, 08 Jan 2009 08:36:16 -0800 |
huffman |
generalize zmod_zmod_cancel -> mod_mod_cancel
|
changeset |
files
|
| Thu, 08 Jan 2009 08:24:08 -0800 |
huffman |
generalize some div/mod lemmas; remove type-specific proofs
|
changeset |
files
|
| Wed, 07 Jan 2009 08:13:56 -0800 |
huffman |
add tracing for domain package proofs
|
changeset |
files
|
| Tue, 06 Jan 2009 11:49:23 -0800 |
huffman |
rename abbreviation square -> power2, to match theorem names
|
changeset |
files
|
| Fri, 09 Jan 2009 08:22:44 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 08 Jan 2009 17:10:41 +0100 |
haftmann |
split of Imperative_HOL theories from HOL-Library
|
changeset |
files
|
| Thu, 08 Jan 2009 17:25:06 +0100 |
haftmann |
NEWS and CONTRIBUTORS
|
changeset |
files
|
| Thu, 08 Jan 2009 10:53:48 +0100 |
haftmann |
dded code_thm antiquotation
|
changeset |
files
|
| Thu, 08 Jan 2009 08:06:11 +0100 |
haftmann |
made SML/NJ happy
|
changeset |
files
|
| Wed, 07 Jan 2009 23:56:56 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Jan 2009 22:33:04 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 07 Jan 2009 22:31:37 +0100 |
haftmann |
tuned siganture of locale.ML
|
changeset |
files
|
| Wed, 07 Jan 2009 22:31:36 +0100 |
haftmann |
tuned signature; internal code reorganisation
|
changeset |
files
|
| Wed, 07 Jan 2009 22:31:36 +0100 |
haftmann |
tuned signature; changed locale predicate name convention
|
changeset |
files
|
| Wed, 07 Jan 2009 22:31:34 +0100 |
haftmann |
changed locale predicate name convention
|
changeset |
files
|
| Wed, 07 Jan 2009 23:53:08 +0100 |
wenzelm |
inductive: added fork_mono flag;
|
changeset |
files
|
| Wed, 07 Jan 2009 23:52:18 +0100 |
wenzelm |
added fork_mono flag, which is usually enabled in batch-mode only;
|
changeset |
files
|
| Wed, 07 Jan 2009 20:27:55 +0100 |
wenzelm |
Proof.global_future_terminal_proof;
|
changeset |
files
|
| Wed, 07 Jan 2009 20:27:23 +0100 |
wenzelm |
Proof.global_future_proof;
|
changeset |
files
|
| Wed, 07 Jan 2009 20:27:05 +0100 |
wenzelm |
future_proof: refined version covers local_future_proof and global_future_proof;
|
changeset |
files
|
| Wed, 07 Jan 2009 17:26:03 +0100 |
wenzelm |
more robust propagation of errors through bulk jobs;
|
changeset |
files
|
| Wed, 07 Jan 2009 16:22:10 +0100 |
wenzelm |
qed/after_qed: singleton result;
|
changeset |
files
|
| Wed, 07 Jan 2009 12:10:22 +0100 |
wenzelm |
Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;
|
changeset |
files
|
| Wed, 07 Jan 2009 12:09:39 +0100 |
wenzelm |
future_terminal_proof: no fork for interactive mode, assert_backward;
|
changeset |
files
|
| Wed, 07 Jan 2009 12:08:22 +0100 |
wenzelm |
added local_theory';
|
changeset |
files
|
| Wed, 07 Jan 2009 08:04:12 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 07 Jan 2009 08:03:25 +0100 |
haftmann |
proper local_theory after Class.class
|
changeset |
files
|
| Tue, 06 Jan 2009 22:08:42 +0100 |
wenzelm |
more parallel loading;
|
changeset |
files
|
| Tue, 06 Jan 2009 21:55:51 +0100 |
wenzelm |
more parallel loading;
|
changeset |
files
|
| Tue, 06 Jan 2009 21:17:43 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 06 Jan 2009 09:18:02 -0800 |
huffman |
merged.
|
changeset |
files
|
| Tue, 06 Jan 2009 09:03:37 -0800 |
huffman |
make cont_proc handle eta-contracted terms
|
changeset |
files
|
| Tue, 06 Jan 2009 09:02:18 -0800 |
huffman |
implement is_closed_term using Term.loose_bvar
|
changeset |
files
|
| Mon, 05 Jan 2009 15:26:57 -0800 |
huffman |
use Thm.close_derivation instead of standard
|
changeset |
files
|
| Tue, 06 Jan 2009 21:17:37 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 06 Jan 2009 14:45:45 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 06 Jan 2009 14:43:35 +0100 |
wenzelm |
renamed structure ParList to Par_List;
|
changeset |
files
|
| Tue, 06 Jan 2009 14:33:49 +0100 |
wenzelm |
parallelized merge_data;
|
changeset |
files
|
| Tue, 06 Jan 2009 13:46:48 +0100 |
wenzelm |
tuned map: reduced overhead due to bulk jobs;
|
changeset |
files
|
| Tue, 06 Jan 2009 13:43:17 +0100 |
wenzelm |
added is_valid;
|
changeset |
files
|
| Tue, 06 Jan 2009 13:36:42 +0100 |
wenzelm |
future_terminal_proof: check Future.enabled;
|
changeset |
files
|
| Tue, 06 Jan 2009 08:50:12 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Jan 2009 08:50:02 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
changeset |
files
|
| Mon, 05 Jan 2009 15:55:51 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
changeset |
files
|
| Mon, 05 Jan 2009 15:55:04 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
changeset |
files
|
| Mon, 05 Jan 2009 15:37:49 +0100 |
haftmann |
removed locale adaption layer
|
changeset |
files
|
| Mon, 05 Jan 2009 15:36:24 +0100 |
haftmann |
rearranged target theories
|
changeset |
files
|
| Mon, 05 Jan 2009 15:35:42 +0100 |
haftmann |
removed locale adaption layer
|
changeset |
files
|
| Mon, 05 Jan 2009 19:37:15 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 05 Jan 2009 18:13:26 +0100 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Mon, 05 Jan 2009 07:54:16 -0800 |
huffman |
merged.
|
changeset |
files
|
| Mon, 29 Dec 2008 11:04:27 -0800 |
huffman |
add lemma psize_unique; simplify some proofs
|
changeset |
files
|
| Mon, 29 Dec 2008 08:31:30 -0800 |
huffman |
minimize imports
|
changeset |
files
|
| Mon, 05 Jan 2009 14:29:26 +0100 |
wenzelm |
parallelize some internal proofs via Proof.future_terminal_proof;
|
changeset |
files
|
| Mon, 05 Jan 2009 14:22:40 +0100 |
wenzelm |
added future_terminal_proof;
|
changeset |
files
|
| Mon, 05 Jan 2009 00:13:11 +0100 |
wenzelm |
Isar.init;
|
changeset |
files
|
| Mon, 05 Jan 2009 00:12:49 +0100 |
wenzelm |
simplified tty model -- back to plain list history, which is independent of editor model;
|
changeset |
files
|
| Mon, 05 Jan 2009 00:10:38 +0100 |
wenzelm |
added is_control, is_regular, is_theory_begin;
|
changeset |
files
|
| Sun, 04 Jan 2009 15:40:30 +0100 |
wenzelm |
more precise is_relevant: requires original main goal, not initial goal state;
|
changeset |
files
|
| Sun, 04 Jan 2009 15:28:40 +0100 |
wenzelm |
tuned protect, conclude: Drule.comp_no_flatten;
|
changeset |
files
|
| Sun, 04 Jan 2009 15:28:09 +0100 |
wenzelm |
added comp_no_flatten;
|
changeset |
files
|
| Sun, 04 Jan 2009 00:01:16 +0100 |
wenzelm |
future proofs: back to Future.fork_pri ~1 for improved parallelism;
|
changeset |
files
|
| Sun, 04 Jan 2009 00:00:03 +0100 |
wenzelm |
cancel: unique threads;
|
changeset |
files
|
| Sat, 03 Jan 2009 21:45:53 +0100 |
wenzelm |
more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;
|
changeset |
files
|
| Sat, 03 Jan 2009 21:44:24 +0100 |
wenzelm |
added eq_group;
|
changeset |
files
|
| Sat, 03 Jan 2009 08:39:54 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sat, 03 Jan 2009 08:39:18 +0100 |
haftmann |
separator, is_qualified
|
changeset |
files
|
| Sat, 03 Jan 2009 08:36:46 +0100 |
haftmann |
added instance for bot, top
|
changeset |
files
|
| Sat, 03 Jan 2009 08:36:20 +0100 |
haftmann |
added binding.ML
|
changeset |
files
|
| Fri, 02 Jan 2009 15:35:11 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 02 Jan 2009 08:15:24 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 02 Jan 2009 08:13:12 +0100 |
haftmann |
improved boostrap order: theory_target.ML before expression.ML
|
changeset |
files
|
| Fri, 02 Jan 2009 08:12:46 +0100 |
haftmann |
named code theorem for Fract_norm
|
changeset |
files
|
| Fri, 02 Jan 2009 23:59:32 +0100 |
wenzelm |
tuned settings;
|
changeset |
files
|
| Fri, 02 Jan 2009 23:36:35 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 02 Jan 2009 22:06:56 +0100 |
krauss |
removed references to OldTerm.*
|
changeset |
files
|
| Fri, 02 Jan 2009 23:28:47 +0100 |
wenzelm |
tuned message_text;
|
changeset |
files
|
| Fri, 02 Jan 2009 23:12:26 +0100 |
wenzelm |
removed obsolete XML mode;
|
changeset |
files
|
| Fri, 02 Jan 2009 23:01:37 +0100 |
wenzelm |
xsymbols: use plain Symbol.output;
|
changeset |
files
|
| Fri, 02 Jan 2009 22:54:04 +0100 |
wenzelm |
Markup.no_output;
|
changeset |
files
|
| Fri, 02 Jan 2009 22:52:42 +0100 |
wenzelm |
added output;
|
changeset |
files
|
| Fri, 02 Jan 2009 22:42:08 +0100 |
wenzelm |
removed unused add_substring;
|
changeset |
files
|
| Fri, 02 Jan 2009 22:41:42 +0100 |
wenzelm |
renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;
|
changeset |
files
|
| Fri, 02 Jan 2009 19:59:26 +0100 |
wenzelm |
removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;
|
changeset |
files
|
| Fri, 02 Jan 2009 19:38:14 +0100 |
wenzelm |
updated rendering of inner token markup;
|
changeset |
files
|
| Fri, 02 Jan 2009 19:38:14 +0100 |
wenzelm |
more detailed inner token markup;
|
changeset |
files
|
| Fri, 02 Jan 2009 19:38:13 +0100 |
wenzelm |
added numeral, which supercedes num, xnum, float;
|
changeset |
files
|
| Fri, 02 Jan 2009 19:30:12 +0100 |
wenzelm |
renamed token markup "_xstr" to "_inner_string";
|
changeset |
files
|
| Fri, 02 Jan 2009 19:29:18 +0100 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Fri, 02 Jan 2009 16:21:47 +0100 |
wenzelm |
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
|
changeset |
files
|
| Fri, 02 Jan 2009 16:21:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:59 +0100 |
wenzelm |
Isar.command: plain Position.id;
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:33 +0100 |
wenzelm |
added type 'a parser, simplified signature;
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:33 +0100 |
wenzelm |
added type 'a parser, simplified signature;
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:33 +0100 |
wenzelm |
added type 'a parser, simplified signature;
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:32 +0100 |
wenzelm |
added props_text (from outer_parse.ML);
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:32 +0100 |
wenzelm |
added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
|
changeset |
files
|
| Fri, 02 Jan 2009 15:44:32 +0100 |
wenzelm |
added id;
|
changeset |
files
|
| Fri, 02 Jan 2009 11:31:40 +0100 |
wenzelm |
MetaSimplifier.SIMPLIFIER;
|
changeset |
files
|
| Fri, 02 Jan 2009 11:31:07 +0100 |
wenzelm |
fixed assumption proof;
|
changeset |
files
|
| Fri, 02 Jan 2009 00:21:59 +0100 |
wenzelm |
tuned header and description of boot files;
|
changeset |
files
|
| Thu, 01 Jan 2009 23:31:59 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Thu, 01 Jan 2009 23:31:49 +0100 |
wenzelm |
normalized some ML type/val aliases;
|
changeset |
files
|
| Thu, 01 Jan 2009 22:57:42 +0100 |
wenzelm |
assumption/close: discontinued implicit prems;
|
changeset |
files
|
| Thu, 01 Jan 2009 22:37:34 +0100 |
wenzelm |
avoid implicit use of prems;
|
changeset |
files
|
| Thu, 01 Jan 2009 22:20:29 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 01 Jan 2009 22:20:08 +0100 |
wenzelm |
eliminated implicit use of prems;
|
changeset |
files
|
| Thu, 01 Jan 2009 21:30:13 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 01 Jan 2009 21:28:38 +0100 |
wenzelm |
updated type 'a lazy;
|
changeset |
files
|
| Thu, 01 Jan 2009 21:27:45 +0100 |
wenzelm |
proper import of ~~/src/HOL/ex/ReflectedFerrack;
|
changeset |
files
|
| Thu, 01 Jan 2009 21:00:33 +0100 |
wenzelm |
crude adaption to intermediate class/locale version;
|
changeset |
files
|
| Thu, 01 Jan 2009 20:56:23 +0100 |
wenzelm |
crude adaption to new locales;
|
changeset |
files
|
| Thu, 01 Jan 2009 20:28:03 +0100 |
wenzelm |
avoid implicit prems -- tuned proofs;
|
changeset |
files
|
| Thu, 01 Jan 2009 17:47:12 +0100 |
wenzelm |
avoid implicit use of prems;
|
changeset |
files
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
Term.add_consts;
|
changeset |
files
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
eliminated OldTerm.(add_)term_consts;
|
changeset |
files
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
eliminated OldTerm.(add_)term_consts;
|
changeset |
files
|
| Thu, 01 Jan 2009 14:23:38 +0100 |
wenzelm |
added canonical add_const_names, add_consts;
|
changeset |
files
|
| Thu, 01 Jan 2009 12:36:37 +0100 |
wenzelm |
provide structure CharVector;
|
changeset |
files
|
| Thu, 01 Jan 2009 12:00:36 +0100 |
wenzelm |
isabelle-process;
|
changeset |
files
|
| Thu, 01 Jan 2009 10:42:48 +0100 |
wenzelm |
updated sessions;
|
changeset |
files
|
| Wed, 31 Dec 2008 20:59:00 +0100 |
wenzelm |
removed unused add_term_free_names;
|
changeset |
files
|
| Wed, 31 Dec 2008 20:31:36 +0100 |
wenzelm |
eliminated OldTerm.add_term_free_names;
|
changeset |
files
|
| Wed, 31 Dec 2008 19:56:38 +0100 |
wenzelm |
updated header;
|
changeset |
files
|
| Wed, 31 Dec 2008 19:54:04 +0100 |
wenzelm |
Term.declare_typ_names, Term.declare_term_frees;
|
changeset |
files
|
| Wed, 31 Dec 2008 19:54:04 +0100 |
wenzelm |
added declare_term_frees;
|
changeset |
files
|
| Wed, 31 Dec 2008 19:54:04 +0100 |
wenzelm |
Term.declare_term_frees;
|
changeset |
files
|
| Wed, 31 Dec 2008 19:54:03 +0100 |
wenzelm |
qualified Term.rename_wrt_term;
|
changeset |
files
|
| Wed, 31 Dec 2008 18:53:19 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
changeset |
files
|
| Wed, 31 Dec 2008 18:53:18 +0100 |
wenzelm |
use fold_aterms directly;
|
changeset |
files
|
| Wed, 31 Dec 2008 18:53:18 +0100 |
wenzelm |
use exists_Const directly;
|
changeset |
files
|
| Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
changeset |
files
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
changeset |
files
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
changeset |
files
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:14 +0100 |
wenzelm |
use exists_subterm directly;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use exists_subterm directly;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:11 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:01:51 +0100 |
wenzelm |
added old_term.ML;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:01:07 +0100 |
wenzelm |
Some old-style term operations.
|
changeset |
files
|
| Tue, 30 Dec 2008 21:49:09 +0100 |
wenzelm |
freeze_thaw: canonical Term.add_XXX operations;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:48:07 +0100 |
wenzelm |
varify: regular name context;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:47:11 +0100 |
wenzelm |
canonical Term.add_var_names, Term.add_tvar_namesT;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:46:48 +0100 |
wenzelm |
canonical Term.add_var_names;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:46:14 +0100 |
wenzelm |
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
|
changeset |
files
|
| Tue, 30 Dec 2008 20:53:21 +0100 |
wenzelm |
removed unused head_name_of;
|
changeset |
files
|
| Tue, 30 Dec 2008 19:08:43 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 30 Dec 2008 19:07:42 +0100 |
wenzelm |
prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;
|
changeset |
files
|
| Tue, 30 Dec 2008 16:50:46 +0100 |
ballarin |
New locales.
|
changeset |
files
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 30 Dec 2008 08:18:54 +0100 |
ballarin |
Temporarily avoid type errors in parse phase.
|
changeset |
files
|
| Tue, 23 Dec 2008 14:29:27 +0100 |
ballarin |
More liberal consistency check for defines elements.
|
changeset |
files
|
| Fri, 19 Dec 2008 16:39:23 +0100 |
ballarin |
All logics ported to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 15:05:37 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 18 Dec 2008 11:16:48 +0100 |
Norbert Schirmer |
adapted statespace module to new locales;
|
changeset |
files
|
| Fri, 19 Dec 2008 14:31:17 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 14:31:07 +0100 |
ballarin |
Intro_locales_tac knows about defines elements; more robust export morphism.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:57:21 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:09:31 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:09:09 +0100 |
ballarin |
More porting to new locales
|
changeset |
files
|
| Thu, 18 Dec 2008 20:19:49 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Wed, 17 Dec 2008 17:53:56 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Wed, 17 Dec 2008 17:53:41 +0100 |
ballarin |
Prevent defines from being checked in interpretation.
|
changeset |
files
|
| Tue, 16 Dec 2008 21:11:39 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Tue, 16 Dec 2008 15:09:37 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 16 Dec 2008 15:09:12 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Mon, 15 Dec 2008 18:12:52 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Sun, 14 Dec 2008 18:45:51 +0100 |
ballarin |
Ported HOL and HOL-Library to new locales.
|
changeset |
files
|
| Sun, 14 Dec 2008 18:45:16 +0100 |
ballarin |
Fixed legacy locale keywords (went to ZF rather than default keywords file).
|
changeset |
files
|
| Sun, 14 Dec 2008 15:50:21 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 12 Dec 2008 20:10:22 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 12 Dec 2008 20:03:30 +0100 |
ballarin |
Porting to new locales.
|
changeset |
files
|
| Fri, 12 Dec 2008 17:00:42 +0100 |
ballarin |
Theory target distinguishes old and new locales.
|
changeset |
files
|
| Fri, 12 Dec 2008 15:02:15 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 12 Dec 2008 14:26:35 +0100 |
ballarin |
Ported to new locales.
|
changeset |
files
|
| Fri, 12 Dec 2008 14:23:49 +0100 |
ballarin |
Merged; updated interpretation command in isar_syn.ML.
|
changeset |
files
|
| Thu, 11 Dec 2008 18:34:05 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:07:36 +0100 |
ballarin |
Add inherited registrations.
|
changeset |
files
|
| Thu, 18 Dec 2008 19:52:11 +0100 |
ballarin |
Refactored: evaluate specification text only in locale declarations.
|
changeset |
files
|
| Wed, 17 Dec 2008 15:21:23 +0100 |
ballarin |
Transfer theorems in print_locale.
|
changeset |
files
|
| Wed, 17 Dec 2008 15:20:33 +0100 |
ballarin |
Attributes not applied in foundational version of fact.
|
changeset |
files
|
| Tue, 16 Dec 2008 20:18:46 +0100 |
ballarin |
Transfer morphism with theory closure.
|
changeset |
files
|
| Tue, 16 Dec 2008 15:08:08 +0100 |
ballarin |
Finer-grained activation so that facts from earlier elements are available.
|
changeset |
files
|
| Tue, 16 Dec 2008 14:29:05 +0100 |
ballarin |
Transfer theorems before activation.
|
changeset |
files
|