| Tue, 20 Oct 2009 20:03:23 +0200 |
wenzelm |
modernized session SET_Protocol;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:52:04 +0200 |
wenzelm |
modernized session Metis_Examples;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:37:09 +0200 |
wenzelm |
modernized session Isar_Examples;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:29:24 +0200 |
wenzelm |
more accurate dependencies for HOL-SMT, which is a session with image;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 10:11:30 +0200 |
boehmes |
added proof reconstructon for Z3,
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 16:03:43 +0200 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 22:47:34 +0200 |
wenzelm |
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
|
file |
diff |
annotate
|
| Thu, 24 Sep 2009 08:28:27 +0200 |
bulwahn |
merged; adopted to changes from Code_Evaluation in the predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
moved predicate compiler to Tools
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 16:01:38 +0200 |
haftmann |
added session theory for Bali and Nominal_Examples
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:33:40 +0200 |
haftmann |
added session entry point theories
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 12:22:53 +0200 |
haftmann |
entry point theory for examples; reactivated half-dead example
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 10:58:25 +0200 |
haftmann |
theory entry point for session Hoare_Parallel (now also with proper underscore)
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 18:13:19 +0200 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:26:51 +0200 |
haftmann |
obey underscore naming convention
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:23:08 +0200 |
haftmann |
generic transfer procedure
|
file |
diff |
annotate
|
| Fri, 04 Sep 2009 13:57:56 +0200 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 21:34:13 +0200 |
boehmes |
merged
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 16:23:53 +0200 |
boehmes |
moved Mirabelle from HOL/Tools to HOL,
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 16:25:44 +0200 |
wenzelm |
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 11:40:28 +0200 |
boehmes |
added further conversions and conversionals
|
file |
diff |
annotate
|
| Fri, 21 Aug 2009 19:06:12 +0200 |
krauss |
fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)
|
file |
diff |
annotate
|
| Thu, 06 Aug 2009 19:51:59 +0200 |
wenzelm |
misc changes to SOS by Philipp Meyer:
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 19:20:24 +0200 |
wenzelm |
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 23:31:11 +0200 |
boehmes |
added Mirabelle
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 21:13:21 +0200 |
chaieb |
merged
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 06:14:25 +0200 |
chaieb |
Moved important theorems from FPS_Examples to FPS --- they are not
|
file |
diff |
annotate
|