| Mon, 28 Feb 2011 15:06:36 +0000 |
paulson |
declare ext [intro]: Extensionality now available by default
|
file |
diff |
annotate
|
| Wed, 23 Feb 2011 11:23:26 +0100 |
noschinl |
setup case_product attribute in HOL and FOL
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Thu, 27 Jan 2011 16:24:29 +0100 |
wenzelm |
CRITICAL markup for critical poking with unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:33:35 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:24:44 +0100 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:58:56 +0100 |
blanchet |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:25:05 +0100 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 17:59:13 +0100 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 18:00:40 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 11:33:17 +0100 |
haftmann |
file for package tool type_mapper carries the same name as its Isar command
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 14:56:07 +0100 |
wenzelm |
simplified HOL.eq simproc matching;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 17:54:15 +0100 |
wenzelm |
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 11:09:18 +0100 |
haftmann |
module for functorial mappers
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 19:14:33 +0200 |
blanchet |
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 11:02:24 +0200 |
krauss |
backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 12:01:04 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 09:17:24 +0200 |
blanchet |
comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 11:11:59 +0200 |
haftmann |
corrected OCaml operator precedence
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 18:43:18 +0200 |
haftmann |
Pure equality is a regular cpde operation
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:33 +0200 |
haftmann |
adjusted to changes in Code_Runtime
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 20:47:14 +0200 |
wenzelm |
dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 16:47:31 +0200 |
haftmann |
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:40:35 +0200 |
haftmann |
Code_Runtime.value, corresponding to ML_Context.value
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:31:32 +0200 |
haftmann |
code_eval renamed to code_runtime
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 11:30:32 +0200 |
haftmann |
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 16:36:23 +0200 |
blanchet |
added Auto Try to the mix of automatic tools
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 19:13:10 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:45:39 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:29:02 +0200 |
blanchet |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:42:50 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:29:47 +0200 |
haftmann |
avoid cyclic modules
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 09:13:28 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 09:13:16 +0200 |
haftmann |
normalization is allowed to solve True
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:51:16 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:29:30 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 00:03:15 +0200 |
blanchet |
finish moving file
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 08:40:25 +0200 |
haftmann |
normalization fails on unchanged goal
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:01:12 +0200 |
haftmann |
tuned text segment
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 21:01:47 +0200 |
blanchet |
fiddling with "try"
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 09:37:43 +0200 |
haftmann |
hide all-too-popular constant name eq
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 12:19:49 +0200 |
haftmann |
prevent line breaks after Scala symbolic operators
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 14:18:09 +0200 |
wenzelm |
discontinued obsolete 'global' and 'local' commands;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:49 +0200 |
haftmann |
refined and unified naming convention for dynamic code evaluation techniques
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:03:07 +0200 |
haftmann |
deglobalized named HOL constants
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 10:27:02 +0200 |
haftmann |
tuned declaration order
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 14:55:09 +0200 |
haftmann |
qualified constants Let and If
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
optional break
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 14:28:22 +0200 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|