| Thu, 02 Sep 2010 17:12:16 +0200 |
wenzelm |
just one refute.ML;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:29:30 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:52:59 +0200 |
blanchet |
move file
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:46:23 +0200 |
blanchet |
shorten a few file names
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 12:01:19 +0200 |
haftmann |
factored out generic part of Scala serializer into code_namespace.ML
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 07:53:31 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:51 +0200 |
bulwahn |
adding Lambda example theory; tuned
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 20:24:28 +0200 |
blanchet |
"try" -- a new diagnosis tool that tries to apply several methods in parallel
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 16:59:49 +0200 |
bulwahn |
adding hotel keycard example for prolog generation
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 19:35:57 +0200 |
hoelzl |
Rewrite the Probability theory.
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:48:30 +0200 |
haftmann |
split and enriched theory SetsAndFunctions
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 16:59:35 +0200 |
haftmann |
removed separate quickcheck_record module
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 16:44:24 +0200 |
haftmann |
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 16:27:58 +0200 |
haftmann |
deleted typecopy package
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:56:43 +0200 |
haftmann |
moved Record.thy from session Plain to Main; avoid variable name acc
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 12:05:48 +0200 |
blanchet |
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
|
file |
diff |
annotate
|
| Tue, 03 Aug 2010 16:57:45 +0200 |
wenzelm |
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
|
file |
diff |
annotate
|
| Sun, 01 Aug 2010 10:15:44 +0200 |
bulwahn |
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 17:27:54 +0200 |
bulwahn |
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
|
file |
diff |
annotate
|
| Wed, 28 Jul 2010 19:04:59 +0200 |
blanchet |
consequence of directory renaming
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:56:01 +0200 |
blanchet |
rename "ATP_Manager" ML module to "Sledgehammer";
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:43:11 +0200 |
blanchet |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:10:35 +0200 |
haftmann |
added Code_Natural.thy
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 18:13:15 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
added new theories to IsaMakefile and ROOT.ML
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 16:50:42 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:43 +0200 |
haftmann |
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:44:36 +0200 |
wenzelm |
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 14:16:12 +0200 |
haftmann |
load cache_io before code generator; moved adhoc-overloading to generic tools
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 00:15:37 +0200 |
krauss |
uniform do notation for monads
|
file |
diff |
annotate
|