| Tue, 28 May 2013 13:22:06 +0200 |
popescua |
merged
|
changeset |
files
|
| Tue, 28 May 2013 13:19:51 +0200 |
popescua |
merged Well_Order_Extension into Zorn
|
changeset |
files
|
| Tue, 28 May 2013 13:14:31 +0200 |
wenzelm |
removed junk (cf. 667961fa6a60);
|
changeset |
files
|
| Tue, 28 May 2013 10:18:43 +0200 |
blanchet |
exported ML function
|
changeset |
files
|
| Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
changeset |
files
|
| Tue, 28 May 2013 08:36:12 +0200 |
blanchet |
clean up list of theorems
|
changeset |
files
|
| Tue, 28 May 2013 08:36:11 +0200 |
blanchet |
removed needless comment (yes, sum_case_if is needed)
|
changeset |
files
|
| Tue, 28 May 2013 08:29:35 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 27 May 2013 22:32:28 +0200 |
wenzelm |
actually test theory Order_Union;
|
changeset |
files
|
| Mon, 27 May 2013 22:30:07 +0200 |
wenzelm |
more direct notation;
|
changeset |
files
|
| Mon, 27 May 2013 22:26:08 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 May 2013 22:25:32 +0200 |
wenzelm |
more literal tokens, e.g. "EX!";
|
changeset |
files
|
| Mon, 27 May 2013 22:00:24 +0200 |
wenzelm |
report markup for ast translations;
|
changeset |
files
|
| Mon, 27 May 2013 21:00:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 27 May 2013 18:39:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 27 May 2013 18:24:38 +0200 |
wenzelm |
discontinued obsolete show_all_types;
|
changeset |
files
|
| Mon, 27 May 2013 20:09:20 +0200 |
popescua |
added Ordered_Union
|
changeset |
files
|
| Fri, 24 May 2013 19:09:56 +0200 |
popescua |
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
|
changeset |
files
|
| Fri, 24 May 2013 18:11:57 +0200 |
popescua |
well-order extension (by Christian Sternagel)
|
changeset |
files
|
| Fri, 24 May 2013 17:37:06 +0200 |
popescua |
modernized Zorn (by Christian Sternagel)
|
changeset |
files
|
| Mon, 27 May 2013 16:53:21 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 May 2013 16:52:39 +0200 |
wenzelm |
more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
|
changeset |
files
|
| Mon, 27 May 2013 15:57:38 +0200 |
wenzelm |
instantiate types as well (see also Thm.first_order_match);
|
changeset |
files
|
| Mon, 27 May 2013 13:55:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 27 May 2013 13:44:02 +0200 |
wenzelm |
updated to ProofGeneral-4.2;
|
changeset |
files
|
| Mon, 27 May 2013 12:40:50 +0200 |
wenzelm |
uniform Term_Position.markers (cf. dbadb4d03cbc);
|
changeset |
files
|
| Mon, 27 May 2013 15:14:41 +0200 |
blanchet |
get rid of "show_all_types" in Nitpick
|
changeset |
files
|
| Mon, 27 May 2013 15:13:34 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 27 May 2013 15:00:01 +0200 |
blanchet |
killed dead argument
|
changeset |
files
|
| Mon, 27 May 2013 14:00:32 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 27 May 2013 13:30:08 +0200 |
blanchet |
generalized "mk_co_iter" to handle mutualized (co)iterators
|
changeset |
files
|
| Mon, 27 May 2013 12:21:17 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 27 May 2013 10:13:51 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 27 May 2013 09:15:26 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 27 May 2013 07:44:10 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 27 May 2013 07:42:10 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 26 May 2013 22:57:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 26 May 2013 22:47:00 +0200 |
wenzelm |
position constraint for bound dummy -- more PIDE markup;
|
changeset |
files
|
| Sun, 26 May 2013 21:53:10 +0200 |
wenzelm |
position constraint for dummy_pattern -- more PIDE markup;
|
changeset |
files
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 26 May 2013 20:42:43 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 26 May 2013 20:08:53 +0200 |
wenzelm |
tuned -- less ML compiler warnings;
|
changeset |
files
|
| Sun, 26 May 2013 20:03:47 +0200 |
wenzelm |
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
|
changeset |
files
|
| Sun, 26 May 2013 19:29:15 +0200 |
wenzelm |
more uniform context;
|
changeset |
files
|
| Sun, 26 May 2013 19:27:32 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 26 May 2013 19:11:52 +0200 |
wenzelm |
more conventional pretty printing;
|
changeset |
files
|
| Sun, 26 May 2013 18:37:43 +0200 |
wenzelm |
tuned white-space;
|
changeset |
files
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
more specific structure for registration into theory and dependency onto locale
|
changeset |
files
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
examples for interpretation into target
|
changeset |
files
|
| Sun, 26 May 2013 14:02:03 +0200 |
blanchet |
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
|
changeset |
files
|
| Sun, 26 May 2013 12:56:37 +0200 |
blanchet |
handle lambda-lifted problems in Isar construction code
|
changeset |
files
|
| Sun, 26 May 2013 11:56:55 +0200 |
nipkow |
simpler proof through custom summation function
|
changeset |
files
|
| Sat, 25 May 2013 18:30:38 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 25 May 2013 17:40:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 17:13:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 17:08:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 16:55:27 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
changeset |
files
|
| Sat, 25 May 2013 15:00:53 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Sat, 25 May 2013 15:44:29 +0200 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
changeset |
files
|