| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
simplified SMT solver code in Sledgehammer
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
changeset |
files
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
changeset |
files
|
| Thu, 31 Jan 2013 17:42:12 +0100 |
hoelzl |
remove unnecessary assumption from real_normed_vector
|
changeset |
files
|
| Thu, 31 Jan 2013 12:09:07 +0100 |
blanchet |
adapted to new MaSh interface
|
changeset |
files
|
| Thu, 31 Jan 2013 11:31:30 +0100 |
hoelzl |
use order topology for extended reals
|
changeset |
files
|
| Thu, 31 Jan 2013 11:31:27 +0100 |
hoelzl |
introduce order topology
|
changeset |
files
|
| Thu, 31 Jan 2013 11:31:22 +0100 |
hoelzl |
simplify heine_borel type class
|
changeset |
files
|
| Thu, 31 Jan 2013 11:20:12 +0100 |
blanchet |
compute proper weight for "p proves p" in MaSh
|
changeset |
files
|
| Tue, 15 Jan 2013 12:13:27 +0100 |
kuncar |
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
|
changeset |
files
|
| Fri, 25 Jan 2013 16:45:09 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 20 Jan 2013 15:34:27 +0100 |
wenzelm |
back to post-release mode -- after fork point;
|
changeset |
files
|
| Wed, 20 Nov 2013 11:01:08 +0100 |
Walther Neuper |
Isabelle2013 --> 2013-1: finished 2013
|
changeset |
files
|
| Tue, 19 Nov 2013 22:23:30 +0000 |
Mathias Lehnfeld |
removed all code concerned with "castab = Unsynchronized.ref"
|
changeset |
files
|
| Tue, 19 Nov 2013 22:18:14 +0000 |
Mathias Lehnfeld |
switched from "castab = Unsynchronized.ref" to Theory_Data
|
changeset |
files
|
| Tue, 19 Nov 2013 21:37:18 +0000 |
Mathias Lehnfeld |
check differences between Theory_Data and "castab = Unsynchronized.ref"
|
changeset |
files
|
| Tue, 19 Nov 2013 20:44:21 +0000 |
Mathias Lehnfeld |
fun spec2str moved.
|
changeset |
files
|
| Tue, 19 Nov 2013 20:08:37 +0000 |
Mathias Lehnfeld |
add functions accessing Theory_Data in parallel to those accessing "castab = Unsynchronized.ref"
|
changeset |
files
|
| Tue, 19 Nov 2013 16:42:06 +0100 |
Walther Neuper |
begin (2) for castab: add functions accessing "Theory_Data"
|
changeset |
files
|
| Wed, 13 Nov 2013 15:10:21 +0100 |
Walther Neuper |
restored tests on Polynomials, cf 11557b906ac1
|
changeset |
files
|
| Wed, 13 Nov 2013 13:01:38 +0000 |
Mathias Lehnfeld |
missing "fun assoc_castab" added
|
changeset |
files
|
| Wed, 13 Nov 2013 12:53:39 +0000 |
Mathias Lehnfeld |
"type spec", "type castab" and "val castab" moved.
|
changeset |
files
|
| Wed, 13 Nov 2013 12:45:24 +0000 |
Mathias Lehnfeld |
~~/src/Tools/isac/Knowledge/GCD_Poly{,_FP} was reloaded by Test_Isac.thy
|
changeset |
files
|
| Tue, 12 Nov 2013 17:48:13 +0100 |
Walther Neuper |
detailed cooperation with TUM shifts from GCD_Poly.thy to the TPPL repository
|
changeset |
files
|
| Tue, 12 Nov 2013 17:40:21 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
| Tue, 12 Nov 2013 17:40:11 +0100 |
Walther Neuper |
keep comments in HOL theories
|
changeset |
files
|
| Mon, 11 Nov 2013 14:55:44 +0000 |
Mathias Lehnfeld |
restrict access to "castab = Unsynchronized.ref"
|
changeset |
files
|
| Fri, 25 Oct 2013 23:23:41 +0100 |
Mathias Lehnfeld |
string_of_calc renamed to check_kestore_calc
|
changeset |
files
|
| Fri, 25 Oct 2013 20:58:28 +0100 |
Mathias Lehnfeld |
removed all code concerned with "calclist' = Unsynchronized.ref"
|
changeset |
files
|
| Fri, 25 Oct 2013 20:52:08 +0100 |
Mathias Lehnfeld |
missing change from c18b813d01cf added
|
changeset |
files
|
| Fri, 25 Oct 2013 19:22:05 +0100 |
Mathias Lehnfeld |
replace "calclist'" in ~~/test/Tools/isac/*
|
changeset |
files
|
| Thu, 24 Oct 2013 17:24:47 +0200 |
Walther Neuper |
removed "rulelist'" also from ~~/test/Tools/isac/*
|
changeset |
files
|
| Thu, 24 Oct 2013 15:00:44 +0200 |
Walther Neuper |
removed all code concerned with "ruleset' = Unsynchronized.ref"
|
changeset |
files
|
| Thu, 24 Oct 2013 14:08:32 +0200 |
Walther Neuper |
notes on "type cal" and "type calc".
|
changeset |
files
|
| Thu, 24 Oct 2013 00:02:29 +0100 |
Mathias Lehnfeld |
switched from "calclist' = Unsynchronized.ref" to Theory_Data
|
changeset |
files
|
| Tue, 22 Oct 2013 17:38:34 +0200 |
Walther Neuper |
replaced Polynomial.thy by version from pre-release website-Isabelle2013-1-RC3
|
changeset |
files
|
| Mon, 21 Oct 2013 15:57:27 +0100 |
Mathias Lehnfeld |
check differences between Theory_Data and "calclist' = Unsynchronized.ref"
|
changeset |
files
|
| Mon, 21 Oct 2013 10:44:08 +0200 |
Walther Neuper |
cleaned notes on tests and todos
|
changeset |
files
|
| Mon, 21 Oct 2013 09:28:01 +0200 |
Walther Neuper |
removed unused code
|
changeset |
files
|
| Mon, 21 Oct 2013 09:03:50 +0200 |
Walther Neuper |
"axiomatization" replaces "axioms" preparing for Isabelle2013-1
|
changeset |
files
|
| Fri, 18 Oct 2013 14:36:51 +0200 |
Walther Neuper |
merged
|
changeset |
files
|
| Fri, 18 Oct 2013 14:36:33 +0200 |
Walther Neuper |
some clean-ups
|
changeset |
files
|
| Wed, 16 Oct 2013 23:59:43 +0100 |
Mathias Lehnfeld |
add functions accessing Theory_Data in parallel to those accessing "calclist' = Unsynchronized.ref
|
changeset |
files
|
| Thu, 10 Oct 2013 19:16:16 +0100 |
Mathias Lehnfeld |
restrict access to "calclist' = Unsynchronized.ref"
|
changeset |
files
|
| Mon, 30 Sep 2013 16:42:52 +0200 |
Walther Neuper |
survey on transition from "ruleset' = Unsynchronized.ref" to Theory_Data
|
changeset |
files
|
| Mon, 30 Sep 2013 16:22:07 +0200 |
Walther Neuper |
switched from "ruleset' = Unsynchronized.ref" to Theory_Data
|
changeset |
files
|
| Mon, 30 Sep 2013 11:50:13 +0200 |
Walther Neuper |
last difference between Theory_Data and "ruleset' = Unsynchronized.ref" removed
|
changeset |
files
|
| Sun, 29 Sep 2013 18:48:35 +0200 |
Walther Neuper |
Thy_Info.get_theory doesn't reliably know ancestor theories
|
changeset |
files
|
| Sun, 29 Sep 2013 18:27:37 +0200 |
Walther Neuper |
collected updates since changeset 9690a8d5f1c
|
changeset |
files
|
| Fri, 27 Sep 2013 17:42:16 +0200 |
Walther Neuper |
Test_Isac needs check for errors in the imported theories in the <Theories> window
|
changeset |
files
|
| Thu, 26 Sep 2013 17:38:01 +0200 |
Walther Neuper |
last but one difference between Theory_Data and "ruleset' = Unsynchronized.ref"
|
changeset |
files
|
| Thu, 26 Sep 2013 15:56:25 +0200 |
Walther Neuper |
one differenc less between Theory_Data and "ruleset' = Unsynchronized.ref"
|
changeset |
files
|
| Thu, 26 Sep 2013 14:52:23 +0200 |
Walther Neuper |
[-Build_Isac] Unsynchronized.ref require specific techniques of investigation
|
changeset |
files
|
| Wed, 25 Sep 2013 13:52:54 +0100 |
Mathias Lehnfeld |
installation dependent files restored.
|
changeset |
files
|
| Wed, 25 Sep 2013 13:33:46 +0100 |
Mathias Lehnfeld |
merged
|
changeset |
files
|