| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:25:17 +0200 |
haftmann |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 13:59:59 +0200 |
bulwahn |
removing the SML evaluator
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 22:55:58 +0200 |
haftmann |
install case certificate for If after code_datatype declaration for bool
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 13:32:33 +0200 |
wenzelm |
simplified BLAST_DATA;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 11:42:43 +0200 |
wenzelm |
modernized functor names;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 21:27:01 +0200 |
wenzelm |
simplified Blast setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 15:05:04 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 14:30:32 +0200 |
wenzelm |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 13:58:13 +0200 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 12:46:48 +0200 |
wenzelm |
clarified simpset setup;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 14:33:33 +0200 |
wenzelm |
explicit context for Codegen.eval_term etc.;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 11:21:12 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 07:44:23 +0200 |
bulwahn |
making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 09:43:36 +0200 |
haftmann |
corrected infix precedence for boolean operators in Haskell
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
file |
diff |
annotate
|
| 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
|