| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 23:02:56 +0200 |
wenzelm |
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 21:28:39 +0200 |
wenzelm |
normalized aliases of Output operations;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 14:00:43 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
removed generation of strange tuple modes in predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
modified predicate compiler further to support tuples
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
modified handling of side conditions in proof procedure of predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 10:25:00 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 15:20:57 +0200 |
haftmann |
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 13:52:18 +0200 |
haftmann |
towards proper handling of argument order in comprehensions
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:45:03 +0200 |
bulwahn |
removing tracing messages in predicate compiler
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
commented rpred compilation; tuned
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
tuned proof procedure; added size-limiting predicate compilation of higher order predicates; added guessing of number parameters for registrating predicates; removed debug messages
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
changed resolving depending predicates and fetching in the predicate compiler
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
refactoring predicate compiler; repaired proof procedure to handle all test cases
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
refactoring predicate compiler; added type synonyms and functions split_smode and split_mode
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
imported patch changed mode inference of predicate compiler to return infered dataflow
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
imported patch generic compilation of predicate compiler with different monads
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 16:48:34 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:27 +0200 |
haftmann |
dropped find_index_eq
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 15:58:12 +0200 |
bulwahn |
commented trancl example; added debug message
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 14:54:30 +0200 |
bulwahn |
exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:33:58 +0200 |
bulwahn |
added diagnostic printing; changed proof for parameters; moved code
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
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, 12 Jun 2009 18:33:58 +0200 |
bulwahn |
added cases to code_pred command
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 21:39:08 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 21:37:26 +0200 |
bulwahn |
improved infrastructure of predicate compiler for adding manual introduction rules
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 14:25:58 +0200 |
wenzelm |
merged, reverting workarounds on both sides;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:48:38 +0200 |
wenzelm |
added sporadic (Local)Theory.checkpoint, to enable parallel proof checking;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:06:13 +0200 |
bulwahn |
making isatest happy; but misunderstanding remains
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 21:04:36 +0200 |
bulwahn |
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 10:42:24 +0200 |
bulwahn |
tuned; corrected exception handling
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 00:46:37 +0200 |
wenzelm |
simplified Graph.extend;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 19:41:27 +0200 |
bulwahn |
avoiding duplicate definitions of executable functions
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 14:20:37 +0200 |
bulwahn |
removed general graph functions in the predicate compiler
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 13:40:57 +0200 |
bulwahn |
removed debug messages
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 12:05:22 +0200 |
bulwahn |
refactoring the predicate compiler
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:00:44 +0200 |
haftmann |
made SML/NJ happy
|
file |
diff |
annotate
|
| Sun, 31 May 2009 17:45:53 +0200 |
wenzelm |
provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
|
file |
diff |
annotate
|
| Thu, 28 May 2009 20:01:38 +0200 |
bulwahn |
added remark to code
|
file |
diff |
annotate
|
| Wed, 20 May 2009 22:24:07 +0200 |
haftmann |
experimental values command
|
file |
diff |
annotate
|
| Mon, 18 May 2009 09:48:06 +0200 |
haftmann |
introduced Thm.generatedK
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:17:59 +0200 |
bulwahn |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
file |
diff |
annotate
|
| Fri, 15 May 2009 15:56:28 +0200 |
bulwahn |
added predicate transformation function for code generation
|
file |
diff |
annotate
|
| Fri, 15 May 2009 15:29:34 +0200 |
bulwahn |
added predicate transformation function for code generation
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:09:36 +0200 |
haftmann |
marginally tuned
|
file |
diff |
annotate
|
| Mon, 11 May 2009 20:09:03 +0200 |
haftmann |
fixed merge accident
|
file |
diff |
annotate
|
| Mon, 11 May 2009 17:20:52 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:39:53 +0200 |
bulwahn |
fixed code_pred command
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:18:42 +0200 |
bulwahn |
Added pred_code command
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 11:10:23 +0200 |
bulwahn |
added general preprocessing of equality in predicates for code generation
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 17:45:16 +0200 |
haftmann |
some experiements towards user interface for predicate compiler
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 14:43:51 +0100 |
haftmann |
NameSpace.base_name ~> Long_Name.base_name
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 09:37:33 +0100 |
haftmann |
binding replaces bstring
|
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
|