| Tue, 27 Jul 2010 23:01:42 +0200 |
wenzelm |
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
|
changeset |
files
|
| Tue, 27 Jul 2010 22:42:53 +0200 |
wenzelm |
avoid repeated File.read for theory text (as before);
|
changeset |
files
|
| Tue, 27 Jul 2010 22:23:32 +0200 |
wenzelm |
tuned messages and comments;
|
changeset |
files
|
| Tue, 27 Jul 2010 22:15:51 +0200 |
wenzelm |
simplified Thy_Header.read -- include Source.of_string_limited here;
|
changeset |
files
|
| Tue, 27 Jul 2010 22:00:26 +0200 |
wenzelm |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
|
changeset |
files
|
| Tue, 27 Jul 2010 12:59:22 +0200 |
wenzelm |
more precise stats;
|
changeset |
files
|
| Mon, 26 Jul 2010 18:25:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 26 Jul 2010 14:44:07 +0200 |
haftmann |
quickcheck images of goals under registration morphisms
|
changeset |
files
|
| Mon, 26 Jul 2010 14:44:07 +0200 |
haftmann |
get_registrations interface
|
changeset |
files
|
| Mon, 26 Jul 2010 11:15:10 +0200 |
haftmann |
restored unusual snd-biased merge/join policy -- required due to non-conservative code setups
|
changeset |
files
|
| Mon, 26 Jul 2010 11:11:10 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 26 Jul 2010 11:10:57 +0200 |
haftmann |
reactivated Scala check
|
changeset |
files
|
| Mon, 26 Jul 2010 11:10:36 +0200 |
haftmann |
corrected range check once more
|
changeset |
files
|
| Mon, 26 Jul 2010 11:10:35 +0200 |
haftmann |
added Code_Natural.thy
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:45 +0200 |
haftmann |
reactivated Scala check; tuned import order
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:45 +0200 |
haftmann |
reactivated Scala check
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:44 +0200 |
haftmann |
modified namespace policy
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:44 +0200 |
haftmann |
use Natural as index type for Haskell and Scala
|
changeset |
files
|
| Sun, 25 Jul 2010 15:43:53 +0200 |
blanchet |
merged
|
changeset |
files
|
| Fri, 23 Jul 2010 21:29:29 +0200 |
blanchet |
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
|
changeset |
files
|
| Fri, 23 Jul 2010 15:04:49 +0200 |
blanchet |
first step in using "fof" rather than "cnf" in TPTP problems
|
changeset |
files
|
| Fri, 23 Jul 2010 14:07:35 +0200 |
blanchet |
fix polymorphic "val"
|
changeset |
files
|
| Sat, 24 Jul 2010 18:08:43 +0200 |
haftmann |
temporarily deactivating check for Scala
|
changeset |
files
|
| Sat, 24 Jul 2010 18:08:41 +0200 |
haftmann |
another refinement chapter in the neverending numeral story
|
changeset |
files
|
| Mon, 26 Jul 2010 17:59:26 +0200 |
wenzelm |
inductive_cases: crude parallelization via Par_List.map;
|
changeset |
files
|
| Mon, 26 Jul 2010 17:41:26 +0200 |
wenzelm |
modernized/unified some specifications;
|
changeset |
files
|
| Mon, 26 Jul 2010 13:50:52 +0200 |
wenzelm |
Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;
|
changeset |
files
|
| Sun, 25 Jul 2010 21:42:39 +0200 |
wenzelm |
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
|
changeset |
files
|
| Sun, 25 Jul 2010 14:41:48 +0200 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
changeset |
files
|
| Sun, 25 Jul 2010 12:57:29 +0200 |
wenzelm |
Thy_Load.check_loaded via Theory.at_end;
|
changeset |
files
|
| Sat, 24 Jul 2010 21:40:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 24 Jul 2010 21:22:21 +0200 |
wenzelm |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
changeset |
files
|
| Sat, 24 Jul 2010 12:14:53 +0200 |
wenzelm |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
|
changeset |
files
|
| Fri, 23 Jul 2010 18:42:46 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 23 Jul 2010 10:58:13 +0200 |
haftmann |
avoid unreliable Haskell Int type
|
changeset |
files
|
| Fri, 23 Jul 2010 10:25:00 +0200 |
haftmann |
proper subclass instead of sublocale
|
changeset |
files
|
| Fri, 23 Jul 2010 09:05:54 +0200 |
haftmann |
repaired tool invocation
|
changeset |
files
|
| Fri, 23 Jul 2010 18:42:35 +0200 |
wenzelm |
observe standard conventions for doc-strings;
|
changeset |
files
|
| Thu, 22 Jul 2010 23:29:39 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:58:18 +0200 |
wenzelm |
eliminated some unused Thy_Info operations;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:50:35 +0200 |
wenzelm |
refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:39:31 +0200 |
wenzelm |
generic external source files -- nothing special about ML here;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:31:20 +0200 |
wenzelm |
discontinued special treatment of ML files -- no longer complete extensions on demand;
|
changeset |
files
|
| Thu, 22 Jul 2010 20:46:45 +0200 |
wenzelm |
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
|
changeset |
files
|
| Thu, 22 Jul 2010 20:36:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
changeset |
files
|
| Thu, 22 Jul 2010 17:26:31 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 22 Jul 2010 17:26:22 +0200 |
haftmann |
dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)
|
changeset |
files
|
| Thu, 22 Jul 2010 16:53:00 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 22 Jul 2010 12:07:30 +0200 |
haftmann |
more generous memory settings for scala check
|
changeset |
files
|
| Thu, 22 Jul 2010 11:29:31 +0200 |
blanchet |
no polymorphic "var"s
|
changeset |
files
|
| Thu, 22 Jul 2010 08:37:46 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 21 Jul 2010 19:21:07 +0200 |
bulwahn |
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
|
changeset |
files
|
| Wed, 21 Jul 2010 21:16:58 +0200 |
blanchet |
do a better job at Skolemizing in Nitpick, for TPTP FOF
|
changeset |
files
|
| Wed, 21 Jul 2010 21:15:49 +0200 |
blanchet |
revert code that was submitted by mistake
|
changeset |
files
|
| Wed, 21 Jul 2010 21:15:07 +0200 |
blanchet |
renamings + only need second component of name pool to reconstruct proofs
|
changeset |
files
|
| Wed, 21 Jul 2010 21:14:47 +0200 |
blanchet |
rename "classrel" to "class_rel"
|
changeset |
files
|
| Wed, 21 Jul 2010 21:14:26 +0200 |
blanchet |
rename "combtyp" constructors
|
changeset |
files
|
| Wed, 21 Jul 2010 21:14:07 +0200 |
blanchet |
renamed "Literal" to "FOLLiteral"
|
changeset |
files
|
| Wed, 21 Jul 2010 21:13:46 +0200 |
blanchet |
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
|
changeset |
files
|
| Wed, 21 Jul 2010 18:13:15 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
fixing quickcheck invocation in HOL-Mirabelle
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
hiding constants in Quickcheck_Types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
adding a type for flat complete lattice to Quickcheck_Types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
added new theories to IsaMakefile and ROOT.ML
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
adding Quickcheck examples for other quickcheck default types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
adding Library theory for other quickcheck default types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
removing obsolete ID in Quickcheck_Examples
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
correcting wellsortedness check and improving error message
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
using multiple default types in quickcheck
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
correcting merging of default_types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
reordering quickcheck signature; exporting test_params and inspection function
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
putting proof in the right context; adding if rewriting; tuned
|
changeset |
files
|
| Thu, 22 Jul 2010 16:43:21 +0200 |
wenzelm |
load_thy: parallel parsing of units, which consist of statement/proof each;
|
changeset |
files
|
| Thu, 22 Jul 2010 14:59:27 +0200 |
wenzelm |
eliminated some unreferenced identifiers;
|
changeset |
files
|
| Thu, 22 Jul 2010 14:01:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 22 Jul 2010 10:41:12 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 21 Jul 2010 21:08:40 +0200 |
wenzelm |
replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
|
changeset |
files
|
| Wed, 21 Jul 2010 20:32:08 +0200 |
wenzelm |
deps_thy/load_thy: store compact text to reduce space by factor 12;
|
changeset |
files
|
| Wed, 21 Jul 2010 17:57:16 +0200 |
wenzelm |
make SML/NJ happy, by adhoc type-constraints;
|
changeset |
files
|
| Wed, 21 Jul 2010 17:55:07 +0200 |
wenzelm |
recovered benchmarks, which are not tested automatically;
|
changeset |
files
|
| Wed, 21 Jul 2010 17:46:36 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Wed, 21 Jul 2010 16:50:42 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 Jul 2010 09:46:36 +0200 |
haftmann |
abstract visualization of locale ingredients; all_locales yields proper locale identifiers
|
changeset |
files
|
| Tue, 20 Jul 2010 14:08:47 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 20 Jul 2010 14:01:06 +0200 |
haftmann |
accomodate for scope of "as" binding in ML
|
changeset |
files
|
| Tue, 20 Jul 2010 10:24:18 +0200 |
haftmann |
tuned code
|
changeset |
files
|
| Tue, 20 Jul 2010 08:54:21 +0200 |
haftmann |
datatype classes are abstract
|
changeset |
files
|
| Tue, 20 Jul 2010 08:54:21 +0200 |
haftmann |
avoid deprecation
|
changeset |
files
|
| Tue, 20 Jul 2010 06:35:29 +0200 |
haftmann |
robustified metis proof
|
changeset |
files
|
| Mon, 19 Jul 2010 20:23:52 +0200 |
haftmann |
modernized abel_cancel simproc setup
|
changeset |
files
|
| Mon, 19 Jul 2010 20:23:49 +0200 |
haftmann |
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
|
changeset |
files
|
| Mon, 19 Jul 2010 20:19:03 +0200 |
haftmann |
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:43 +0200 |
haftmann |
dropped essentially ineffective tuning
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:43 +0200 |
haftmann |
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
|
changeset |
files
|
| Mon, 19 Jul 2010 12:17:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 19 Jul 2010 12:17:30 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:44 +0200 |
haftmann |
distinguish different classes of const syntax
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:43 +0200 |
haftmann |
Scala: subtle difference in printing strings vs. complex mixfix syntax
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
check code generation for Scala
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
dropped superfluous prefixes
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
optional break
|
changeset |
files
|
| Fri, 16 Jul 2010 15:55:32 +0200 |
haftmann |
consolidate const_syntax naming
|
changeset |
files
|
| Wed, 21 Jul 2010 16:49:52 +0200 |
wenzelm |
recovered benchmarks, which are not tested automatically;
|
changeset |
files
|
| Wed, 21 Jul 2010 16:29:20 +0200 |
wenzelm |
reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;
|
changeset |
files
|
| Wed, 21 Jul 2010 16:14:16 +0200 |
wenzelm |
eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Wed, 21 Jul 2010 15:31:38 +0200 |
wenzelm |
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
|
changeset |
files
|
| Wed, 21 Jul 2010 15:23:46 +0200 |
wenzelm |
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
|
changeset |
files
|
| Wed, 21 Jul 2010 15:13:36 +0200 |
wenzelm |
explicit dependency on theory HOL;
|
changeset |
files
|
| Wed, 21 Jul 2010 15:02:51 +0200 |
wenzelm |
ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
|
changeset |
files
|
| Wed, 21 Jul 2010 14:27:05 +0200 |
wenzelm |
added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
|
changeset |
files
|
| Wed, 21 Jul 2010 13:55:44 +0200 |
wenzelm |
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;
|
changeset |
files
|
| Wed, 21 Jul 2010 13:25:14 +0200 |
wenzelm |
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
|
changeset |
files
|
| Tue, 20 Jul 2010 23:16:21 +0200 |
wenzelm |
qualified Thy_Info.get_theory;
|
changeset |
files
|
| Tue, 20 Jul 2010 23:09:49 +0200 |
wenzelm |
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
|
changeset |
files
|
| Tue, 20 Jul 2010 22:03:37 +0200 |
wenzelm |
further Mac OS X deviations;
|
changeset |
files
|
| Tue, 20 Jul 2010 21:57:26 +0200 |
wenzelm |
warning in proper transaction context;
|
changeset |
files
|
| Tue, 20 Jul 2010 21:49:39 +0200 |
wenzelm |
SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here;
|
changeset |
files
|
| Tue, 20 Jul 2010 21:07:23 +0200 |
wenzelm |
avoid duplicate printing of 'theory' state (cf. 173974e07dea);
|
changeset |
files
|
| Tue, 20 Jul 2010 20:56:28 +0200 |
wenzelm |
toplevel pp for Proof.state and Toplevel.state;
|
changeset |
files
|
| Tue, 20 Jul 2010 20:10:27 +0200 |
wenzelm |
execute document version at high priority;
|
changeset |
files
|
| Tue, 20 Jul 2010 18:33:19 +0200 |
wenzelm |
Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
|
changeset |
files
|
| Tue, 20 Jul 2010 18:19:50 +0200 |
wenzelm |
edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;
|
changeset |
files
|
| Tue, 20 Jul 2010 17:35:42 +0200 |
wenzelm |
back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c);
|
changeset |
files
|
| Tue, 20 Jul 2010 16:42:48 +0200 |
wenzelm |
export Graph.get_entry for convenience;
|
changeset |
files
|
| Tue, 20 Jul 2010 14:44:33 +0200 |
wenzelm |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
|
changeset |
files
|
| Tue, 20 Jul 2010 14:41:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 20 Jul 2010 11:11:15 +0200 |
wenzelm |
observe follow_caret (again);
|
changeset |
files
|
| Mon, 19 Jul 2010 22:19:18 +0200 |
wenzelm |
Session: predefined real time parameters;
|
changeset |
files
|
| Mon, 19 Jul 2010 08:59:43 +0200 |
haftmann |
bind and then latex symbols
|
changeset |
files
|
| Sun, 18 Jul 2010 17:56:04 +0200 |
wenzelm |
minor update of dependencies;
|
changeset |
files
|
| Fri, 16 Jul 2010 15:28:23 +0200 |
haftmann |
corrected range chec
|
changeset |
files
|
| Fri, 16 Jul 2010 15:28:22 +0200 |
haftmann |
first roughly working version of Imperative HOL for Scala
|
changeset |
files
|
| Fri, 16 Jul 2010 14:11:08 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 16 Jul 2010 13:58:37 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 16 Jul 2010 13:58:29 +0200 |
haftmann |
a first sketch for Imperative HOL witht Scala
|
changeset |
files
|
| Fri, 16 Jul 2010 13:57:46 +0200 |
haftmann |
don't fail gracefully
|
changeset |
files
|
| Fri, 16 Jul 2010 13:57:29 +0200 |
haftmann |
restored long-broken syntax sanity checks
|
changeset |
files
|
| Fri, 16 Jul 2010 13:57:29 +0200 |
haftmann |
tuned interpunctation
|
changeset |
files
|
| Fri, 16 Jul 2010 10:23:21 +0200 |
haftmann |
fragments of Scala
|
changeset |
files
|
| Thu, 15 Jul 2010 10:16:17 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 15 Jul 2010 10:12:49 +0200 |
haftmann |
adjusted; fixed typo
|
changeset |
files
|
| Thu, 15 Jul 2010 08:14:05 +0200 |
haftmann |
dropped spurious export_code
|
changeset |
files
|
| Wed, 14 Jul 2010 19:10:23 +0100 |
kleing |
use different log server (macbroy23 down)
|
changeset |
files
|
| Wed, 14 Jul 2010 17:27:54 +0200 |
haftmann |
more consistent spacing in generated monadic code
|
changeset |
files
|
| Wed, 14 Jul 2010 17:16:02 +0200 |
haftmann |
braced needed in layout-insensitive syntax
|
changeset |
files
|
| Wed, 14 Jul 2010 17:15:58 +0200 |
haftmann |
repaired some implementations of imperative operations
|
changeset |
files
|
| Wed, 14 Jul 2010 16:45:30 +0200 |
haftmann |
repaired reference implementation for OCaml
|
changeset |
files
|
| Wed, 14 Jul 2010 16:45:30 +0200 |
haftmann |
part of pervasive test
|
changeset |
files
|
| Wed, 14 Jul 2010 16:45:30 +0200 |
haftmann |
avoid ambiguities; tuned
|
changeset |
files
|
| Wed, 14 Jul 2010 16:45:29 +0200 |
haftmann |
repaired of_list implementation for SML, OCaml
|
changeset |
files
|
| Wed, 14 Jul 2010 16:13:14 +0200 |
haftmann |
avoid export_code ... file -
|
changeset |
files
|
| Wed, 14 Jul 2010 16:02:50 +0200 |
haftmann |
explicit optional checking
|
changeset |
files
|
| Wed, 14 Jul 2010 15:49:29 +0200 |
haftmann |
added Isar syntax for code checking
|
changeset |
files
|
| Wed, 14 Jul 2010 15:49:29 +0200 |
haftmann |
corrected import
|
changeset |
files
|
| Wed, 14 Jul 2010 15:08:02 +0200 |
haftmann |
use generic description slot for formal code checking
|
changeset |
files
|
| Wed, 14 Jul 2010 14:53:44 +0200 |
haftmann |
formal slot for code checker
|
changeset |
files
|
| Wed, 14 Jul 2010 14:53:44 +0200 |
haftmann |
export_code without file prints to standard output
|
changeset |
files
|
| Wed, 14 Jul 2010 14:20:47 +0200 |
haftmann |
check without explicit path
|
changeset |
files
|
| Wed, 14 Jul 2010 14:16:12 +0200 |
haftmann |
load cache_io before code generator; moved adhoc-overloading to generic tools
|
changeset |
files
|
| Wed, 14 Jul 2010 12:27:44 +0200 |
haftmann |
tuned infix syntax
|
changeset |
files
|
| Wed, 14 Jul 2010 12:27:44 +0200 |
haftmann |
dropped M suffix; added predicate monad bind
|
changeset |
files
|
| Wed, 14 Jul 2010 12:27:43 +0200 |
haftmann |
self-built symbol for part of bind operator
|
changeset |
files
|
| Wed, 14 Jul 2010 09:42:44 +0200 |
haftmann |
redirect stderr to stdout
|
changeset |
files
|
| Tue, 13 Jul 2010 21:07:12 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 11:27:19 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 11:26:16 +0100 |
paulson |
corrected mixfix declarations and tidied proofs
|
changeset |
files
|
| Tue, 13 Jul 2010 17:19:35 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 17:19:08 +0100 |
paulson |
Fixed syntax and tidied some proofs
|
changeset |
files
|
| Tue, 13 Jul 2010 18:01:42 +0200 |
bulwahn |
correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
|
changeset |
files
|
| Tue, 13 Jul 2010 16:30:13 +0200 |
haftmann |
consolidated names of theorems
|
changeset |
files
|
| Tue, 13 Jul 2010 16:21:49 +0200 |
haftmann |
qualified names for (really) all array operations
|
changeset |
files
|
| Tue, 13 Jul 2010 16:12:40 +0200 |
haftmann |
canonical argument order for get
|
changeset |
files
|
| Tue, 13 Jul 2010 16:00:56 +0200 |
haftmann |
qualified names for (almost) all array operations
|
changeset |
files
|
| Tue, 13 Jul 2010 15:37:31 +0200 |
haftmann |
canonical argument order for present
|
changeset |
files
|
| Tue, 13 Jul 2010 15:34:02 +0200 |
haftmann |
canonical argument order for length
|
changeset |
files
|
| Tue, 13 Jul 2010 11:23:21 +0100 |
kleing |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 11:21:22 +0100 |
kleing |
new crontab
|
changeset |
files
|
| Tue, 13 Jul 2010 12:20:23 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 12:16:24 +0200 |
haftmann |
proper merge of operation changes and generic do-syntax
|
changeset |
files
|
| Tue, 13 Jul 2010 12:05:20 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 12:01:34 +0200 |
haftmann |
hide_const; update replaces change
|
changeset |
files
|
| Tue, 13 Jul 2010 11:17:13 +0100 |
kleing |
remove separate afp settings again, use plain mac-poly64-M4 instead.
|
changeset |
files
|
| Tue, 13 Jul 2010 11:01:12 +0100 |
kleing |
merged
|
changeset |
files
|
| Tue, 13 Jul 2010 11:00:20 +0100 |
kleing |
new settings for afp test
|
changeset |
files
|
| Tue, 13 Jul 2010 12:00:11 +0200 |
krauss |
Heap_Monad uses Monad_Syntax
|
changeset |
files
|
| Tue, 13 Jul 2010 11:50:22 +0200 |
krauss |
State_Monad uses Monad_Syntax
|
changeset |
files
|
| Tue, 13 Jul 2010 00:15:37 +0200 |
krauss |
uniform do notation for monads
|
changeset |
files
|
| Tue, 13 Jul 2010 00:15:37 +0200 |
krauss |
generic ad-hoc overloading via check/uncheck
|
changeset |
files
|
| Tue, 13 Jul 2010 11:38:04 +0200 |
haftmann |
corrected title
|
changeset |
files
|
| Tue, 13 Jul 2010 11:38:03 +0200 |
haftmann |
theorem collections do not contain default rules any longer
|
changeset |
files
|
| Tue, 13 Jul 2010 02:29:05 +0200 |
boehmes |
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
|
changeset |
files
|
| Mon, 12 Jul 2010 22:35:41 +0200 |
wenzelm |
removed unused/untested IOA 'automaton' package;
|
changeset |
files
|
| Mon, 12 Jul 2010 22:17:31 +0200 |
wenzelm |
removed impractical tolerate_legacy_features flag;
|
changeset |
files
|
| Mon, 12 Jul 2010 22:14:11 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Mon, 12 Jul 2010 22:07:36 +0200 |
wenzelm |
removed legacy aliases;
|
changeset |
files
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
changeset |
files
|
| Mon, 12 Jul 2010 21:12:18 +0200 |
wenzelm |
eliminated OldGoals.strip_context;
|
changeset |
files
|
| Mon, 12 Jul 2010 20:35:10 +0200 |
wenzelm |
removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
|
changeset |
files
|
| Mon, 12 Jul 2010 20:21:39 +0200 |
wenzelm |
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
|
changeset |
files
|
| Mon, 12 Jul 2010 18:59:38 +0200 |
wenzelm |
some modernization of really ancient Meson experiments;
|
changeset |
files
|
| Mon, 12 Jul 2010 16:40:48 +0200 |
haftmann |
dropped empty theory
|
changeset |
files
|
| Mon, 12 Jul 2010 16:38:20 +0200 |
haftmann |
moved auxiliary lemma
|
changeset |
files
|
| Mon, 12 Jul 2010 16:26:48 +0200 |
haftmann |
dropped unused lemmas of dubious value
|
changeset |
files
|
| Mon, 12 Jul 2010 16:23:30 +0200 |
haftmann |
dropped unused lemmas of dubious value
|
changeset |
files
|
| Mon, 12 Jul 2010 16:19:15 +0200 |
haftmann |
split off mrec into separate theory
|
changeset |
files
|
| Mon, 12 Jul 2010 16:05:08 +0200 |
haftmann |
spelt out relational framework in a consistent way
|
changeset |
files
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
changeset |
files
|
| Mon, 12 Jul 2010 11:21:56 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 12 Jul 2010 11:21:27 +0200 |
haftmann |
moved co-regularity to class section; avoid duplicated class_deps
|
changeset |
files
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
changeset |
files
|
| Mon, 12 Jul 2010 08:58:27 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
changeset |
files
|
| Mon, 12 Jul 2010 08:58:12 +0200 |
haftmann |
more regular session structure
|
changeset |
files
|
| Sat, 10 Jul 2010 22:39:16 +0200 |
wenzelm |
regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;
|
changeset |
files
|
| Sat, 10 Jul 2010 21:38:16 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jul 2010 16:44:05 +0100 |
kleing |
Added current crontab of macbroy28
|
changeset |
files
|
| Fri, 09 Jul 2010 17:15:03 +0200 |
krauss |
moved example to its own file in HOL/ex
|
changeset |
files
|
| Fri, 09 Jul 2010 17:00:42 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 09 Jul 2010 16:58:44 +0200 |
haftmann |
pervasive success combinator
|
changeset |
files
|
| Fri, 09 Jul 2010 16:32:25 +0200 |
krauss |
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
|
changeset |
files
|
| Fri, 09 Jul 2010 10:08:10 +0200 |
haftmann |
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
|
changeset |
files
|
| Fri, 09 Jul 2010 09:48:54 +0200 |
haftmann |
adapted to changes
|
changeset |
files
|
| Fri, 09 Jul 2010 09:48:53 +0200 |
haftmann |
guard combinator
|
changeset |
files
|
| Fri, 09 Jul 2010 09:48:53 +0200 |
haftmann |
tuned reference theory
|
changeset |
files
|
| Fri, 09 Jul 2010 09:48:52 +0200 |
haftmann |
tuned array theory
|
changeset |
files
|
| Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
changeset |
files
|
| Thu, 08 Jul 2010 17:23:05 +0200 |
haftmann |
dropped ancient in-place compilation of SML; more tests
|
changeset |
files
|
| Thu, 08 Jul 2010 16:48:33 +0200 |
haftmann |
updated documentation
|
changeset |
files
|
| Thu, 08 Jul 2010 16:41:57 +0200 |
haftmann |
dropped ancient in-place compilation of SML
|
changeset |
files
|
| Thu, 08 Jul 2010 16:28:18 +0200 |
haftmann |
more accurate dependencies
|
changeset |
files
|
| Thu, 08 Jul 2010 16:20:03 +0200 |
haftmann |
empty default
|
changeset |
files
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
checking generated code for various target languages
|
changeset |
files
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
changeset |
files
|
| Thu, 08 Jul 2010 16:19:23 +0200 |
haftmann |
tuned module names
|
changeset |
files
|
| Thu, 08 Jul 2010 16:17:44 +0200 |
haftmann |
tuned tabs
|
changeset |
files
|
| Thu, 08 Jul 2010 16:17:44 +0200 |
haftmann |
tuned script
|
changeset |
files
|
| Thu, 08 Jul 2010 09:36:23 +0200 |
haftmann |
combinator with_tmp_dir
|
changeset |
files
|
| Thu, 08 Jul 2010 09:36:22 +0200 |
haftmann |
rm_tree: remove entire file system trees
|
changeset |
files
|
| Wed, 07 Jul 2010 18:17:23 +0200 |
berghofe |
Boxes may now have different widths.
|
changeset |
files
|
| Wed, 07 Jul 2010 09:26:54 +0200 |
hoelzl |
tuned
|
changeset |
files
|
| Wed, 07 Jul 2010 08:25:23 +0200 |
bulwahn |
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
|
changeset |
files
|
| Wed, 07 Jul 2010 08:25:22 +0200 |
bulwahn |
added NEWS entry
|
changeset |
files
|
| Wed, 07 Jul 2010 08:25:21 +0200 |
bulwahn |
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
|
changeset |
files
|
| Tue, 06 Jul 2010 08:08:35 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 05 Jul 2010 09:14:51 -0700 |
huffman |
generalize type of is_interval to class euclidean_space
|
changeset |
files
|
| Mon, 05 Jul 2010 09:12:35 -0700 |
huffman |
section -> subsection
|
changeset |
files
|
| Sun, 04 Jul 2010 09:26:30 -0700 |
huffman |
generalize some lemmas about derivatives
|
changeset |
files
|
| Sun, 04 Jul 2010 09:25:17 -0700 |
huffman |
uniqueness of Frechet derivative
|
changeset |
files
|
| Tue, 06 Jul 2010 21:33:14 +0200 |
wenzelm |
implode pseudo utf8, i.e. decode byte-stuffed low ASCII characters;
|
changeset |
files
|
| Tue, 06 Jul 2010 10:02:24 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 06 Jul 2010 09:27:49 +0200 |
haftmann |
even more fun with primrec
|
changeset |
files
|