| Fri, 15 May 2009 16:52:28 +0200 |
haftmann |
experimental addition of quickcheck
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:17 +0200 |
haftmann |
dropped theory Term_Of_Syntax
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:47 +0200 |
haftmann |
split Predicate_Compile examples into separate theory
|
file |
diff |
annotate
|
| Tue, 12 May 2009 20:07:05 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:32:49 +0100 |
chaieb |
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Fri, 08 May 2009 09:48:07 +0200 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| Thu, 07 May 2009 12:17:17 +0200 |
haftmann |
added theory for explicit equivalence relation in preorders
|
file |
diff |
annotate
|
| Wed, 06 May 2009 19:09:31 +0200 |
haftmann |
proper structures for list and string code generation stuff
|
file |
diff |
annotate
|
| Wed, 06 May 2009 16:01:06 +0200 |
haftmann |
refined HOL string theories and corresponding ML fragments
|
file |
diff |
annotate
|
| Mon, 04 May 2009 14:49:51 +0200 |
haftmann |
removed code_name module
|
file |
diff |
annotate
|
| Sat, 25 Apr 2009 21:28:04 +0200 |
wenzelm |
misc cleanup of auto_solve and quickcheck:
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 17:45:17 +0200 |
haftmann |
observe distinction between Pure/Tools and Tools more closely
|
file |
diff |
annotate
|
| Mon, 20 Apr 2009 09:32:40 +0200 |
haftmann |
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:52:37 +0200 |
haftmann |
code generator bootstrap theory src/Tools/Code_Generator.thy
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:34:54 +0200 |
haftmann |
wrecked old code_funcgr module
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:30:39 +0200 |
haftmann |
theory NatBin now named Nat_Numeral
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 19:01:17 +0100 |
haftmann |
moved Imperative_HOL examples to Imperative_HOL/ex
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:11 +0100 |
haftmann |
dropped theory Arith_Tools
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 23:01:25 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 14:27:21 +0100 |
nipkow |
optional latex sugar
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 20:11:06 +0100 |
wenzelm |
basic setup for "main" as generated Isabelle manual;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 11:41:14 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 11:40:58 +0100 |
nipkow |
Docs
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
moved Decision_Procs examples to Decision_Procs/ex
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 22:56:39 +0100 |
wenzelm |
added session HOL-Docs;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 15:25:28 +0100 |
haftmann |
added predicate compiler, as formally checked prototype, not as user package
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 20:30:16 +0100 |
haftmann |
constructive version of Cantor's first diagonalization argument
|
file |
diff |
annotate
|