| Thu, 09 Nov 2006 18:58:52 +0100 |
webertj |
timing/tracing code removed
|
changeset |
files
|
| Thu, 09 Nov 2006 18:48:45 +0100 |
webertj |
interpreters for fst and snd added
|
changeset |
files
|
| Thu, 09 Nov 2006 16:14:43 +0100 |
webertj |
new CCS-based implementation that should work with PolyML 5.0
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:51 +0100 |
wenzelm |
HOL: less/less_eq on bool, modified syntax;
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:50 +0100 |
wenzelm |
removed obsolete locale_results;
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:47 +0100 |
wenzelm |
imports Binimial;
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:45 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:43 +0100 |
wenzelm |
lfp_induct_set;
|
changeset |
files
|
| Thu, 09 Nov 2006 11:58:13 +0100 |
wenzelm |
modified less/less_eq syntax to avoid "x < y < z" etc.;
|
changeset |
files
|
| Thu, 09 Nov 2006 00:43:12 +0100 |
huffman |
added lemma mult_mono'
|
changeset |
files
|
| Thu, 09 Nov 2006 00:19:16 +0100 |
huffman |
added LIM_norm and related lemmas
|
changeset |
files
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
changeset |
files
|
| Wed, 08 Nov 2006 22:24:54 +0100 |
krauss |
added profiling code, improved handling of proof terms, generation of domain
|
changeset |
files
|
| Wed, 08 Nov 2006 21:45:15 +0100 |
wenzelm |
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
|
changeset |
files
|
| Wed, 08 Nov 2006 21:45:14 +0100 |
wenzelm |
case_tr': proper handling of authentic consts;
|
changeset |
files
|
| Wed, 08 Nov 2006 21:45:13 +0100 |
wenzelm |
removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);
|
changeset |
files
|
| Wed, 08 Nov 2006 19:48:36 +0100 |
haftmann |
renamed DatatypeHooks.invoke to all
|
changeset |
files
|
| Wed, 08 Nov 2006 19:48:35 +0100 |
haftmann |
moved lemma eq_neq_eq_imp_neq to HOL
|
changeset |
files
|
| Wed, 08 Nov 2006 19:48:34 +0100 |
haftmann |
renamed Lattice_Locales to Lattices
|
changeset |
files
|
| Wed, 08 Nov 2006 19:46:10 +0100 |
haftmann |
abstract ordering theories
|
changeset |
files
|
| Wed, 08 Nov 2006 13:51:03 +0100 |
wenzelm |
obsolete (cf. ROOT.ML);
|
changeset |
files
|
| Wed, 08 Nov 2006 13:48:35 +0100 |
wenzelm |
added structure Main (from Main.ML);
|
changeset |
files
|
| Wed, 08 Nov 2006 13:48:34 +0100 |
wenzelm |
proper definition of add_zero_left/right;
|
changeset |
files
|
| Wed, 08 Nov 2006 13:48:33 +0100 |
wenzelm |
removed NatArith.thy, Main.ML;
|
changeset |
files
|
| Wed, 08 Nov 2006 13:48:29 +0100 |
wenzelm |
removed theory NatArith (now part of Nat);
|
changeset |
files
|
| Wed, 08 Nov 2006 11:23:09 +0100 |
wenzelm |
* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".
|
changeset |
files
|
| Wed, 08 Nov 2006 11:22:40 +0100 |
wenzelm |
moved contribution note to CONTRIBUTORS;
|
changeset |
files
|
| Wed, 08 Nov 2006 09:08:54 +0100 |
krauss |
Made "termination by lexicographic_order" the default for "fun" definitions.
|
changeset |
files
|
| Wed, 08 Nov 2006 02:13:02 +0100 |
huffman |
LIM_compose -> isCont_LIM_compose;
|
changeset |
files
|
| Wed, 08 Nov 2006 00:34:15 +0100 |
huffman |
generalized types of of_nat and of_int to work with non-commutative types
|
changeset |
files
|
| Tue, 07 Nov 2006 22:06:32 +0100 |
krauss |
untabified
|
changeset |
files
|
| Tue, 07 Nov 2006 21:30:03 +0100 |
wenzelm |
complex goal statements: misc cleanup;
|
changeset |
files
|
| Tue, 07 Nov 2006 21:28:14 +0100 |
krauss |
Added datatype hook to declare all case_congs as "fundef_cong" automatically.
|
changeset |
files
|
| Tue, 07 Nov 2006 19:40:56 +0100 |
wenzelm |
removed obsolete theorem statements (cf. specification.ML);
|
changeset |
files
|
| Tue, 07 Nov 2006 19:40:13 +0100 |
wenzelm |
tuned specifications;
|
changeset |
files
|
| Tue, 07 Nov 2006 19:39:54 +0100 |
wenzelm |
fixed locale fact references;
|
changeset |
files
|
| Tue, 07 Nov 2006 19:39:53 +0100 |
wenzelm |
removed obsolete print_state_hook;
|
changeset |
files
|
| Tue, 07 Nov 2006 19:39:52 +0100 |
wenzelm |
theorem statements: incorporate Obtain.statement, tuned;
|
changeset |
files
|
| Tue, 07 Nov 2006 19:39:50 +0100 |
wenzelm |
moved statement to specification.ML;
|
changeset |
files
|
| Tue, 07 Nov 2006 19:39:48 +0100 |
wenzelm |
removed obsolete Locale.smart_theorem;
|
changeset |
files
|
| Tue, 07 Nov 2006 19:39:46 +0100 |
wenzelm |
avoid handling of arbitrary exceptions;
|
changeset |
files
|
| Tue, 07 Nov 2006 18:25:48 +0100 |
schirmer |
field-update in records is generalised to take a function on the field
|
changeset |
files
|
| Tue, 07 Nov 2006 18:14:53 +0100 |
schirmer |
exported intro_locales_tac
|
changeset |
files
|
| Tue, 07 Nov 2006 16:21:54 +0100 |
paulson |
Proper theorem names at last, no fakes!!
|
changeset |
files
|
| Tue, 07 Nov 2006 15:07:02 +0100 |
haftmann |
some corrections
|
changeset |
files
|
| Tue, 07 Nov 2006 14:49:09 +0100 |
haftmann |
adjusted title
|
changeset |
files
|
| Tue, 07 Nov 2006 14:30:03 +0100 |
wenzelm |
simplified dest_eq;
|
changeset |
files
|
| Tue, 07 Nov 2006 14:30:00 +0100 |
wenzelm |
commented out parts which have been inactive (unintentionally) for a long time;
|
changeset |
files
|
| Tue, 07 Nov 2006 14:29:58 +0100 |
wenzelm |
removed obsolete dest_eq_typ;
|
changeset |
files
|
| Tue, 07 Nov 2006 14:29:57 +0100 |
wenzelm |
tuned hypsubst setup;
|
changeset |
files
|
| Tue, 07 Nov 2006 14:14:36 +0100 |
haftmann |
continued
|
changeset |
files
|
| Tue, 07 Nov 2006 14:03:06 +0100 |
haftmann |
made locale partial_order compatible with axclass order; changed import order; consecutive changes
|
changeset |
files
|
| Tue, 07 Nov 2006 14:03:04 +0100 |
haftmann |
made locale partial_order compatible with axclass order
|
changeset |
files
|
| Tue, 07 Nov 2006 14:02:10 +0100 |
haftmann |
adjusted two lemma names due to name change in interpretation
|
changeset |
files
|
| Tue, 07 Nov 2006 14:02:08 +0100 |
haftmann |
changed import order
|
changeset |
files
|
| Tue, 07 Nov 2006 12:20:11 +0100 |
krauss |
Added a (stub of a) function tutorial
|
changeset |
files
|
| Tue, 07 Nov 2006 11:53:55 +0100 |
krauss |
Preparations for making "lexicographic_order" part of "fun"
|
changeset |
files
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
changeset |
files
|
| Tue, 07 Nov 2006 11:47:56 +0100 |
wenzelm |
'const_syntax' command: allow fixed variables, renamed to 'notation';
|
changeset |
files
|
| Tue, 07 Nov 2006 11:46:50 +0100 |
wenzelm |
replaced const_syntax by notation, which operates on terms;
|
changeset |
files
|
| Tue, 07 Nov 2006 11:46:49 +0100 |
wenzelm |
Isar.context: proper error;
|
changeset |
files
|
| Tue, 07 Nov 2006 11:46:48 +0100 |
wenzelm |
replaced const_syntax by notation, which operates on terms;
|
changeset |
files
|
| Tue, 07 Nov 2006 11:46:47 +0100 |
wenzelm |
read_const: include type;
|
changeset |
files
|
| Tue, 07 Nov 2006 11:46:46 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
changeset |
files
|
| Tue, 07 Nov 2006 11:46:45 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 07 Nov 2006 11:28:25 +0100 |
berghofe |
Adapted to changes in FixedPoint theory.
|
changeset |
files
|
| Tue, 07 Nov 2006 09:59:43 +0100 |
krauss |
method exported
|
changeset |
files
|
| Tue, 07 Nov 2006 09:41:14 +0100 |
krauss |
updated NEWS
|
changeset |
files
|
| Tue, 07 Nov 2006 09:33:47 +0100 |
krauss |
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
|
changeset |
files
|
| Tue, 07 Nov 2006 08:03:46 +0100 |
haftmann |
added gfx
|
changeset |
files
|
| Mon, 06 Nov 2006 16:29:21 +0100 |
haftmann |
dropped blastdata.ML
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:37 +0100 |
haftmann |
(adjustions)
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:36 +0100 |
haftmann |
two further lemmas on split
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:35 +0100 |
haftmann |
removed dependency of ord on eq
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:34 +0100 |
haftmann |
removed itrev as inlining theorem
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:33 +0100 |
haftmann |
added state monad to HOL library
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:31 +0100 |
haftmann |
code generator module naming improved
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:30 +0100 |
haftmann |
(continued)
|
changeset |
files
|
| Mon, 06 Nov 2006 16:28:29 +0100 |
haftmann |
(continued)
|
changeset |
files
|
| Mon, 06 Nov 2006 12:04:44 +0100 |
krauss |
minor cleanup
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:42 +0100 |
wenzelm |
case_tr: do not intern already internal consts;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:41 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:40 +0100 |
wenzelm |
removed isactrlconst;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:39 +0100 |
wenzelm |
instantiate: avoid global references;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:37 +0100 |
wenzelm |
added const_syntax_name;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:35 +0100 |
wenzelm |
removed obsolete first_duplicate;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:34 +0100 |
wenzelm |
added syntax_name;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:33 +0100 |
wenzelm |
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
|
changeset |
files
|
| Sun, 05 Nov 2006 21:44:32 +0100 |
wenzelm |
Sign.const_syntax_name;
|
changeset |
files
|
| Sun, 05 Nov 2006 09:36:25 +0100 |
haftmann |
added gfx
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:43 +0100 |
wenzelm |
removed checkpoint interface;
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:43 +0100 |
wenzelm |
String.compare: slow version -- performance test;
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:41 +0100 |
wenzelm |
replaced apply_copy by apply';
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:41 +0100 |
wenzelm |
removed is_Trueprop (use can dest_Trueprop'' instead);
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:40 +0100 |
wenzelm |
removed is_Trueprop (use can dest_Trueprop'' instead);
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:39 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:38 +0100 |
wenzelm |
HOL_USEDIR_OPTIONS: -p 1 by default;
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 04 Nov 2006 19:25:34 +0100 |
wenzelm |
* October 2006: Stefan Hohe, TUM;
|
changeset |
files
|
| Sat, 04 Nov 2006 13:19:04 +0100 |
wenzelm |
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
|
changeset |
files
|
| Sat, 04 Nov 2006 12:53:35 +0100 |
wenzelm |
optional argument for timespan (default 100);
|
changeset |
files
|
| Sat, 04 Nov 2006 12:46:40 +0100 |
wenzelm |
added at-mac-poly-e, at64-poly-e;
|
changeset |
files
|
| Sat, 04 Nov 2006 00:12:06 +0100 |
huffman |
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
|
changeset |
files
|
| Sat, 04 Nov 2006 00:11:11 +0100 |
huffman |
new Deriv.thy contains stuff from Lim.thy
|
changeset |
files
|
| Fri, 03 Nov 2006 15:28:13 +0100 |
haftmann |
re-added simpdata.ML
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:48 +0100 |
haftmann |
new ML serializer
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:47 +0100 |
haftmann |
fixed problem with eta-expansion
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:46 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:45 +0100 |
haftmann |
fixed problem with variable names
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:44 +0100 |
haftmann |
tightened notion of function equations
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:43 +0100 |
haftmann |
dropped name_mangler.ML
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:42 +0100 |
haftmann |
some example tweaking
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:41 +0100 |
haftmann |
added particular test for partially applied case constants
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:40 +0100 |
haftmann |
improved evaluation setup
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:39 +0100 |
haftmann |
adapted to changes in codegen_data.ML
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:38 +0100 |
haftmann |
added code gen II
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:37 +0100 |
haftmann |
simplified reasoning tools setup
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:36 +0100 |
haftmann |
dropped prop_cs
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:35 +0100 |
haftmann |
dropped equals_conv for nbe
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:34 +0100 |
haftmann |
first version of style guide
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:33 +0100 |
haftmann |
continued tutorial
|
changeset |
files
|
| Fri, 03 Nov 2006 14:22:31 +0100 |
haftmann |
added serialization keywords
|
changeset |
files
|
| Thu, 02 Nov 2006 14:27:18 +0100 |
dixon |
bugfix to zipto: left and right were wrong way around.
|
changeset |
files
|
| Thu, 02 Nov 2006 13:35:09 +0100 |
nipkow |
added sum_squared
|
changeset |
files
|
| Wed, 01 Nov 2006 19:07:37 +0100 |
urbanc |
changed a misplaced "also" to a "moreover" (caused a loop somehow)
|
changeset |
files
|
| Wed, 01 Nov 2006 19:03:30 +0100 |
urbanc |
changed to not compile Iteration and Recursion, but Lam_Funs instead
|
changeset |
files
|
| Wed, 01 Nov 2006 17:57:02 +0100 |
huffman |
move DERIV_sumr from Series.thy to Lim.thy
|
changeset |
files
|
| Wed, 01 Nov 2006 17:14:16 +0100 |
huffman |
generalize type of lemma isCont_Id
|
changeset |
files
|
| Wed, 01 Nov 2006 16:48:58 +0100 |
huffman |
new proof of Bseq_NSbseq using transfer
|
changeset |
files
|
| Wed, 01 Nov 2006 16:11:31 +0100 |
urbanc |
changed to use Lam_Funs
|
changeset |
files
|
| Wed, 01 Nov 2006 15:51:11 +0100 |
paulson |
clauses for iff-introduction, unfortunately useless
|
changeset |
files
|
| Wed, 01 Nov 2006 15:50:19 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Wed, 01 Nov 2006 15:49:43 +0100 |
paulson |
Numerous cosmetic changes.
|
changeset |
files
|
| Wed, 01 Nov 2006 15:45:44 +0100 |
urbanc |
not needed anymore
|
changeset |
files
|
| Wed, 01 Nov 2006 15:44:31 +0100 |
urbanc |
these files are superseded by the internal recursion combinator and the file Lam_Funs.thy
|
changeset |
files
|
| Wed, 01 Nov 2006 15:39:20 +0100 |
paulson |
More blacklisting
|
changeset |
files
|
| Wed, 01 Nov 2006 08:46:54 +0100 |
bulwahn |
added lexicographic_order tactic
|
changeset |
files
|
| Tue, 31 Oct 2006 14:59:27 +0100 |
haftmann |
new SML serializer
|
changeset |
files
|
| Tue, 31 Oct 2006 14:59:26 +0100 |
haftmann |
clarified make_term interface
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:23 +0100 |
haftmann |
introduced CodegenData.add_func_legacy
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:16 +0100 |
haftmann |
cleaned up
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:14 +0100 |
haftmann |
adapted seralizer syntax
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:12 +0100 |
haftmann |
adapted to new serializer syntax
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:18 +0100 |
haftmann |
constructing proof
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:17 +0100 |
haftmann |
dropped constructiv `->
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:16 +0100 |
haftmann |
new serialization syntax; experimental extensions
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:14 +0100 |
haftmann |
refined
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:13 +0100 |
haftmann |
refined algorithm
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:12 +0100 |
haftmann |
simplified preprocessor framework
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:11 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:08 +0100 |
haftmann |
*** empty log message ***
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:06 +0100 |
haftmann |
fixed type signature of Type.varify
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:01 +0100 |
haftmann |
dropped junk
|
changeset |
files
|
| Tue, 31 Oct 2006 09:28:57 +0100 |
haftmann |
disabled some code generation (an intermeidate solution)
|
changeset |
files
|
| Tue, 31 Oct 2006 09:28:56 +0100 |
haftmann |
adapted to new serializer syntax
|
changeset |
files
|
| Tue, 31 Oct 2006 09:28:55 +0100 |
haftmann |
added Equals_conv
|
changeset |
files
|
| Tue, 31 Oct 2006 09:28:54 +0100 |
haftmann |
cleaned up
|
changeset |
files
|
| Tue, 31 Oct 2006 09:28:53 +0100 |
haftmann |
adaptions to changes in preprocessor
|
changeset |
files
|
| Tue, 31 Oct 2006 09:28:52 +0100 |
haftmann |
dropped nth_update
|
changeset |
files
|
| Mon, 30 Oct 2006 16:42:46 +0100 |
paulson |
Purely cosmetic
|
changeset |
files
|
| Mon, 30 Oct 2006 13:07:51 +0100 |
urbanc |
new file for defining functions in the lambda-calculus
|
changeset |
files
|
| Thu, 26 Oct 2006 16:08:40 +0200 |
krauss |
Added "recdef_wf" and "simp" attribute to "wf_measures"
|
changeset |
files
|
| Thu, 26 Oct 2006 15:46:39 +0200 |
krauss |
Removed debugging output
|
changeset |
files
|
| Thu, 26 Oct 2006 15:16:31 +0200 |
krauss |
removed free "x" from termination goal...
|
changeset |
files
|
| Thu, 26 Oct 2006 15:12:03 +0200 |
krauss |
Added "measures" combinator for lexicographic combinations of multiple measures.
|
changeset |
files
|
| Thu, 26 Oct 2006 10:48:35 +0200 |
paulson |
Conversion to clause form now tolerates Boolean variables without looping.
|
changeset |
files
|
| Tue, 24 Oct 2006 12:02:53 +0200 |
urbanc |
adapted to Stefan's new inductive package
|
changeset |
files
|
| Mon, 23 Oct 2006 17:46:11 +0200 |
krauss |
Fixed bug in the handling of congruence rules
|
changeset |
files
|
| Mon, 23 Oct 2006 16:56:35 +0200 |
haftmann |
(added entry)
|
changeset |
files
|
| Mon, 23 Oct 2006 16:49:21 +0200 |
haftmann |
switched merge_alists'' to AList.merge'' whenever appropriate
|
changeset |
files
|
| Mon, 23 Oct 2006 11:18:50 +0200 |
paulson |
new single-step proofs
|
changeset |
files
|
| Mon, 23 Oct 2006 11:18:25 +0200 |
paulson |
meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
|
changeset |
files
|
| Mon, 23 Oct 2006 11:17:29 +0200 |
paulson |
Improved tracing
|
changeset |
files
|
| Mon, 23 Oct 2006 11:17:24 +0200 |
haftmann |
fixed two bugs
|
changeset |
files
|
| Mon, 23 Oct 2006 11:05:33 +0200 |
haftmann |
bugfixes
|
changeset |
files
|
| Mon, 23 Oct 2006 11:05:08 +0200 |
haftmann |
added example with split
|
changeset |
files
|
| Mon, 23 Oct 2006 11:05:07 +0200 |
haftmann |
cleanup in ML setup code
|
changeset |
files
|
| Mon, 23 Oct 2006 11:05:06 +0200 |
haftmann |
added option of Haskell serializer
|
changeset |
files
|
| Mon, 23 Oct 2006 11:05:05 +0200 |
haftmann |
continued
|
changeset |
files
|
| Mon, 23 Oct 2006 00:52:15 +0200 |
berghofe |
Added freshness context to FCBs.
|
changeset |
files
|
| Mon, 23 Oct 2006 00:51:16 +0200 |
berghofe |
Adapted to changes in FCBs.
|
changeset |
files
|
| Mon, 23 Oct 2006 00:48:45 +0200 |
berghofe |
Added Compile and Height examples.
|
changeset |
files
|
| Mon, 23 Oct 2006 00:47:25 +0200 |
berghofe |
Added Compile and Height examples to Nominal directory.
|
changeset |
files
|
| Fri, 20 Oct 2006 18:22:24 +0200 |
haftmann |
removed antisym_setup.ML
|
changeset |
files
|
| Fri, 20 Oct 2006 18:20:22 +0200 |
haftmann |
cleaned up
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:47 +0200 |
haftmann |
final Haskell serializer
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:46 +0200 |
haftmann |
dropped classop shallow namespace
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:41 +0200 |
haftmann |
added Haskell
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:27 +0200 |
haftmann |
added reserved words for Haskell
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:26 +0200 |
haftmann |
slight cleanup
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:25 +0200 |
haftmann |
extended section on code generator
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:24 +0200 |
haftmann |
small refinements
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:23 +0200 |
haftmann |
continued
|
changeset |
files
|
| Fri, 20 Oct 2006 17:07:22 +0200 |
haftmann |
added entries for tutorials
|
changeset |
files
|
| Fri, 20 Oct 2006 14:13:48 +0200 |
berghofe |
Proof of "bs # fK bs us vs" no longer depends on FCBs.
|
changeset |
files
|
| Fri, 20 Oct 2006 11:07:45 +0200 |
paulson |
example of a single-step proof reconstruction
|
changeset |
files
|
| Fri, 20 Oct 2006 11:06:20 +0200 |
paulson |
Fixed the "exception Empty" bug in elim2Fol
|
changeset |
files
|
| Fri, 20 Oct 2006 11:04:15 +0200 |
paulson |
Added more debugging info
|
changeset |
files
|
| Fri, 20 Oct 2006 11:03:33 +0200 |
paulson |
nclauses no longer requires its input to be in NNF
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:56 +0200 |
haftmann |
cleanup
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:55 +0200 |
haftmann |
explicit change of code width possible
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:53 +0200 |
haftmann |
code nofunc now permits theorems violating typing discipline
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:51 +0200 |
haftmann |
abandoned foldl
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:47 +0200 |
haftmann |
fold cleanup
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:42 +0200 |
haftmann |
slight cleanup
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:39 +0200 |
haftmann |
slight adaption
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:38 +0200 |
haftmann |
added normal post setup; cleaned up "execution" constants
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:37 +0200 |
haftmann |
added normal post setup
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:36 +0200 |
haftmann |
added if_delayed
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:35 +0200 |
haftmann |
started tutorial
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:34 +0200 |
haftmann |
code_constsubst -> code_axioms
|
changeset |
files
|
| Fri, 20 Oct 2006 10:44:33 +0200 |
haftmann |
Symtab.foldl replaced by Symtab.fold
|
changeset |
files
|
| Thu, 19 Oct 2006 12:08:27 +0200 |
berghofe |
Induction rule for graph of recursion combinator
|
changeset |
files
|
| Thu, 19 Oct 2006 11:21:01 +0200 |
berghofe |
Split up FCBs into separate formulae for each binder.
|
changeset |
files
|
| Wed, 18 Oct 2006 23:15:16 +0200 |
urbanc |
cleaning up
|
changeset |
files
|
| Wed, 18 Oct 2006 23:06:51 +0200 |
urbanc |
adapted to Stefan's new inductive package and cleaning up
|
changeset |
files
|
| Wed, 18 Oct 2006 16:13:03 +0200 |
krauss |
Switched function package to use the new package for inductive predicates.
|
changeset |
files
|
| Wed, 18 Oct 2006 10:15:39 +0200 |
paulson |
More robust error handling in make_nnf and forward_res
|
changeset |
files
|
| Wed, 18 Oct 2006 10:07:36 +0200 |
ballarin |
Stylistic improvements.
|
changeset |
files
|
| Tue, 17 Oct 2006 09:51:04 +0200 |
berghofe |
Restructured and repaired code dealing with case names
|
changeset |
files
|
| Tue, 17 Oct 2006 02:40:21 +0200 |
kleing |
macbroy6 still has non-standard setup
|
changeset |
files
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
changeset |
files
|
| Mon, 16 Oct 2006 14:07:21 +0200 |
haftmann |
slight cleanup
|
changeset |
files
|
| Mon, 16 Oct 2006 14:07:20 +0200 |
haftmann |
fixed print translations for bounded quantification
|
changeset |
files
|
| Mon, 16 Oct 2006 14:07:19 +0200 |
haftmann |
added explicit print translation for nat_case
|
changeset |
files
|
| Mon, 16 Oct 2006 14:07:18 +0200 |
haftmann |
added isactrlconst
|
changeset |
files
|
| Mon, 16 Oct 2006 10:27:54 +0200 |
ballarin |
Order and lattice structures no longer based on records.
|
changeset |
files
|
| Sun, 15 Oct 2006 12:16:20 +0200 |
isatest |
add experimental macbroy6 (intel-darwin)
|
changeset |
files
|
| Sun, 15 Oct 2006 12:03:57 +0200 |
isatest |
add experimental at64 poly-4.9.1 test on atbroy101
|
changeset |
files
|
| Sun, 15 Oct 2006 11:47:13 +0200 |
kleing |
generate devel snapshot even if experimental builds fail.
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:56 +0200 |
wenzelm |
added peek;
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:55 +0200 |
wenzelm |
added theorem(_i);
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:54 +0200 |
wenzelm |
export map_elem;
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:53 +0200 |
wenzelm |
added assert;
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:51 +0200 |
wenzelm |
theorem: added local_theory version;
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:51 +0200 |
wenzelm |
Attrib.pretty_attrib;
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:50 +0200 |
wenzelm |
added pretty_attribs (from attrib.ML);
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:48 +0200 |
wenzelm |
moved pretty_attribs to attrib.ML;
|
changeset |
files
|
| Sat, 14 Oct 2006 23:25:46 +0200 |
wenzelm |
locale begin/end;
|
changeset |
files
|