| Thu, 05 Nov 2009 15:44:39 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 15:24:49 +0100 |
boehmes |
handle let expressions inside terms by unfolding (instead of raising an exception),
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:48:40 +0100 |
boehmes |
shorter names for variables and verification conditions,
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:37:39 +0100 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 17:17:30 +0100 |
krauss |
added Tree23 to IsaMakefile
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:54:24 +0100 |
boehmes |
added HOL-Boogie
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:49 +0100 |
haftmann |
moved Commutative_Ring into session Decision_Procs
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 01:32:06 +0100 |
krauss |
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 18:17:26 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:06:15 +0100 |
wenzelm |
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 08:14:39 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 18:21:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 11:43:06 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 11:42:31 +0000 |
paulson |
New theory Probability, which contains a development of measure theory
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 14:46:03 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 12:59:57 +0000 |
paulson |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 19:03:59 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 18:09:11 +0100 |
boehmes |
removed unused file smt_builtin.ML,
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 20:04:20 +0100 |
wenzelm |
recovered sort indentation for "sort position", as documented in the file;
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 14:57:49 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 14:21:20 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 09:14:29 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 14:51:47 +0200 |
blanchet |
added Nitpick's theory and ML files to Isabelle/HOL;
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 14:54:43 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 14:53:33 +0100 |
berghofe |
Added Pattern.thy to Nominal/Examples.
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 11:30:08 +0100 |
wenzelm |
more precise dependencies, notably for HOL-Multivariate_Analysis;
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 09:03:57 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 13:23:18 +0200 |
himmelma |
distinguished session for multivariate analysis
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:37:56 +0200 |
krauss |
renamed auto_term.ML -> relation.ML
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 15:33:19 +0200 |
krauss |
renamed FundefDatatype -> Function_Fun
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 17:12:47 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 17:12:36 +0200 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 14:33:07 +0200 |
krauss |
pat_completeness gets its own file
|
file |
diff |
annotate
|
| 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
|
| Wed, 22 Jul 2009 18:02:10 +0200 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 09:24:50 +0200 |
krauss |
move Kleene_Algebra to Library
|
file |
diff |
annotate
|
| Fri, 03 Jul 2009 16:51:08 +0200 |
haftmann |
nominal.ML is nominal_datatype.ML
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:18:55 +0200 |
haftmann |
renamed theory Code_Set to Fset
|
file |
diff |
annotate
|
| Thu, 25 Jun 2009 17:07:18 +0200 |
haftmann |
added List_Set and Code_Set theories
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:46:54 +0200 |
wenzelm |
standard naming conventions for session and theories;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:08:33 +0200 |
haftmann |
NewNumberTheory depends on Algebra
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 10:22:11 +0200 |
chaieb |
Added Library/Fraction_Field.thy: The fraction field of any integral
|
file |
diff |
annotate
|
| Mon, 22 Jun 2009 23:48:24 +0200 |
wenzelm |
observe standard theory naming conventions;
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 15:47:41 +0200 |
nipkow |
fixed NewNumberTheory deps
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 21:08:07 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 18:33:10 +0200 |
nipkow |
Added NewNumberTheory by Jeremy Avigad
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 16:55:01 -0700 |
huffman |
new GCD library, courtesy of Jeremy Avigad
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 15:04:33 +0200 |
haftmann |
separate directory for datatype package
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 22:59:54 +0200 |
haftmann |
first running version of qc generators for datatypes
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 16:55:20 +0200 |
haftmann |
added trees implementing mappings
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 15:53:07 +0200 |
haftmann |
tuned code generator test theories
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:04:03 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:00:29 +0200 |
berghofe |
Added Convex_Euclidean_Space.thy again.
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 07:45:49 -0700 |
huffman |
add dependency on Limits.thy
|
file |
diff |
annotate
|
| Thu, 28 May 2009 18:59:51 +0200 |
himmelma |
Removed Convex_Euclidean_Space.thy from Library.
|
file |
diff |
annotate
|
| Thu, 28 May 2009 13:56:50 +0200 |
himmelma |
Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
|
file |
diff |
annotate
|
| Tue, 26 May 2009 17:29:32 +0200 |
haftmann |
separate module for quickcheck generators
|
file |
diff |
annotate
|
| Tue, 19 May 2009 16:54:55 +0200 |
haftmann |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file |
diff |
annotate
|
| Tue, 19 May 2009 13:57:32 +0200 |
haftmann |
moved Code_Index, Random and Quickcheck before Main
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:16:49 +0200 |
haftmann |
experimental move of Quickcheck and related theories to HOL image
|
file |
diff |
annotate
|
| 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
|