Sat, 13 May 2006 02:51:47 +0200 defs (unchecked overloaded), including former primrec;
wenzelm [Sat, 13 May 2006 02:51:47 +0200] rev 19634
defs (unchecked overloaded), including former primrec; tuned;
Sat, 13 May 2006 02:51:46 +0200 updated;
wenzelm [Sat, 13 May 2006 02:51:46 +0200] rev 19633
updated;
Sat, 13 May 2006 02:51:45 +0200 add_defs: unchecked flag;
wenzelm [Sat, 13 May 2006 02:51:45 +0200] rev 19632
add_defs: unchecked flag; tuned;
Sat, 13 May 2006 02:51:43 +0200 'defs': unchecked flag;
wenzelm [Sat, 13 May 2006 02:51:43 +0200] rev 19631
'defs': unchecked flag;
Sat, 13 May 2006 02:51:42 +0200 Theory.add_defs(_i): added unchecked flag;
wenzelm [Sat, 13 May 2006 02:51:42 +0200] rev 19630
Theory.add_defs(_i): added unchecked flag;
Sat, 13 May 2006 02:51:40 +0200 added add_defs_unchecked(_i);
wenzelm [Sat, 13 May 2006 02:51:40 +0200] rev 19629
added add_defs_unchecked(_i);
Sat, 13 May 2006 02:51:37 +0200 actually reject malformed defs;
wenzelm [Sat, 13 May 2006 02:51:37 +0200] rev 19628
actually reject malformed defs; added unchecked flag; tuned;
Sat, 13 May 2006 02:51:35 +0200 moved defs explanation to isar-ref;
wenzelm [Sat, 13 May 2006 02:51:35 +0200] rev 19627
moved defs explanation to isar-ref;
Sat, 13 May 2006 02:51:33 +0200 added defs (unchecked)'';
wenzelm [Sat, 13 May 2006 02:51:33 +0200] rev 19626
added defs (unchecked)''; more explanations on well-formednes of defs;
Sat, 13 May 2006 02:51:30 +0200 * Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm [Sat, 13 May 2006 02:51:30 +0200] rev 19625
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
Fri, 12 May 2006 18:11:09 +0200 tuned;
wenzelm [Fri, 12 May 2006 18:11:09 +0200] rev 19624
tuned;
Fri, 12 May 2006 11:19:41 +0200 added lemma in_measure
nipkow [Fri, 12 May 2006 11:19:41 +0200] rev 19623
added lemma in_measure
Fri, 12 May 2006 10:38:00 +0200 fixed silly bug in function serializer for ML
haftmann [Fri, 12 May 2006 10:38:00 +0200] rev 19622
fixed silly bug in function serializer for ML
Fri, 12 May 2006 04:20:02 +0200 add new finite chain theorems
huffman [Fri, 12 May 2006 04:20:02 +0200] rev 19621
add new finite chain theorems
Fri, 12 May 2006 01:01:08 +0200 improved propagate_deps;
wenzelm [Fri, 12 May 2006 01:01:08 +0200] rev 19620
improved propagate_deps; removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;
Thu, 11 May 2006 21:46:17 +0200 check result against certified prop, i.e. admit non-normal statements;
wenzelm [Thu, 11 May 2006 21:46:17 +0200] rev 19619
check result against certified prop, i.e. admit non-normal statements;
Thu, 11 May 2006 19:19:33 +0200 tuned;
wenzelm [Thu, 11 May 2006 19:19:33 +0200] rev 19618
tuned;
Thu, 11 May 2006 19:19:31 +0200 avoid raw equality on type thm;
wenzelm [Thu, 11 May 2006 19:19:31 +0200] rev 19617
avoid raw equality on type thm;
Thu, 11 May 2006 19:15:16 +0200 replaced Graph.fold_nodes by general Graph.fold;
wenzelm [Thu, 11 May 2006 19:15:16 +0200] rev 19616
replaced Graph.fold_nodes by general Graph.fold;
Thu, 11 May 2006 19:15:15 +0200 added fold;
wenzelm [Thu, 11 May 2006 19:15:15 +0200] rev 19615
added fold; removed fold_nodes; added IntGraph; tuned;
Thu, 11 May 2006 19:15:14 +0200 tuned Defs.merge;
wenzelm [Thu, 11 May 2006 19:15:14 +0200] rev 19614
tuned Defs.merge;
Thu, 11 May 2006 19:15:13 +0200 allow dependencies of disjoint collections of instances;
wenzelm [Thu, 11 May 2006 19:15:13 +0200] rev 19613
allow dependencies of disjoint collections of instances; major cleanup;
Thu, 11 May 2006 19:15:12 +0200 use IntGraph from Pure;
wenzelm [Thu, 11 May 2006 19:15:12 +0200] rev 19612
use IntGraph from Pure;
Thu, 11 May 2006 15:46:40 +0200 Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug"
krauss [Thu, 11 May 2006 15:46:40 +0200] rev 19611
Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug" due to abbreviations
Thu, 11 May 2006 11:11:05 +0200 Fix: Auto term must apply wf-intro rules repeatedly.
krauss [Thu, 11 May 2006 11:11:05 +0200] rev 19610
Fix: Auto term must apply wf-intro rules repeatedly.
Thu, 11 May 2006 10:25:55 +0200 fixed codegen bug, cleanup
haftmann [Thu, 11 May 2006 10:25:55 +0200] rev 19609
fixed codegen bug, cleanup
Wed, 10 May 2006 16:23:21 +0200 revert accidental text change;
wenzelm [Wed, 10 May 2006 16:23:21 +0200] rev 19608
revert accidental text change;
Tue, 09 May 2006 14:18:40 +0200 introduced characters for code generator; some improved code lemmas for some list functions
haftmann [Tue, 09 May 2006 14:18:40 +0200] rev 19607
introduced characters for code generator; some improved code lemmas for some list functions
Tue, 09 May 2006 11:00:32 +0200 added .cvsignore
haftmann [Tue, 09 May 2006 11:00:32 +0200] rev 19606
added .cvsignore
Tue, 09 May 2006 10:13:09 +0200 added ExecutableRat.thy
haftmann [Tue, 09 May 2006 10:13:09 +0200] rev 19605
added ExecutableRat.thy
Tue, 09 May 2006 10:11:47 +0200 removed 1::int
haftmann [Tue, 09 May 2006 10:11:47 +0200] rev 19604
removed 1::int
Tue, 09 May 2006 10:11:30 +0200 added preprocs for CodegenTheorems
haftmann [Tue, 09 May 2006 10:11:30 +0200] rev 19603
added preprocs for CodegenTheorems
Tue, 09 May 2006 10:10:57 +0200 improved code generation for wfrec
haftmann [Tue, 09 May 2006 10:10:57 +0200] rev 19602
improved code generation for wfrec
Tue, 09 May 2006 10:10:28 +0200 added codegen preprocessors for numerals
haftmann [Tue, 09 May 2006 10:10:28 +0200] rev 19601
added codegen preprocessors for numerals
Tue, 09 May 2006 10:10:12 +0200 adaption to CodegenTheorems
haftmann [Tue, 09 May 2006 10:10:12 +0200] rev 19600
adaption to CodegenTheorems
Tue, 09 May 2006 10:09:37 +0200 added DatatypeHooks
haftmann [Tue, 09 May 2006 10:09:37 +0200] rev 19599
added DatatypeHooks
Tue, 09 May 2006 10:09:17 +0200 different object logic setup for CodegenTheorems
haftmann [Tue, 09 May 2006 10:09:17 +0200] rev 19598
different object logic setup for CodegenTheorems
Tue, 09 May 2006 10:08:20 +0200 major refinement of codegen_theorems.ML
haftmann [Tue, 09 May 2006 10:08:20 +0200] rev 19597
major refinement of codegen_theorems.ML
Tue, 09 May 2006 10:07:38 +0200 removed superfluous eq_ord
haftmann [Tue, 09 May 2006 10:07:38 +0200] rev 19596
removed superfluous eq_ord
Tue, 09 May 2006 09:18:05 +0200 improved chmod/chgrp handling
haftmann [Tue, 09 May 2006 09:18:05 +0200] rev 19595
improved chmod/chgrp handling
Mon, 08 May 2006 21:40:40 +0200 speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman [Mon, 08 May 2006 21:40:40 +0200] rev 19594
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
Mon, 08 May 2006 17:40:25 +0200 quoted 'termination' command;
wenzelm [Mon, 08 May 2006 17:40:25 +0200] rev 19593
quoted 'termination' command;
Mon, 08 May 2006 17:40:08 +0200 Defs.define: const_typargs;
wenzelm [Mon, 08 May 2006 17:40:08 +0200] rev 19592
Defs.define: const_typargs;
Mon, 08 May 2006 17:40:07 +0200 added raw_string_of_sort/typ/term;
wenzelm [Mon, 08 May 2006 17:40:07 +0200] rev 19591
added raw_string_of_sort/typ/term;
Mon, 08 May 2006 17:40:06 +0200 simple substructure test for typargs (independent type constructors);
wenzelm [Mon, 08 May 2006 17:40:06 +0200] rev 19590
simple substructure test for typargs (independent type constructors);
Mon, 08 May 2006 17:40:05 +0200 tuned;
wenzelm [Mon, 08 May 2006 17:40:05 +0200] rev 19589
tuned;
Mon, 08 May 2006 12:23:57 +0200 string_of_option tuned
webertj [Mon, 08 May 2006 12:23:57 +0200] rev 19588
string_of_option tuned
Sun, 07 May 2006 00:47:07 +0200 * Isar: removed obsolete 'concl is' patterns.
wenzelm [Sun, 07 May 2006 00:47:07 +0200] rev 19587
* Isar: removed obsolete 'concl is' patterns.
Sun, 07 May 2006 00:44:50 +0200 removed 'concl is' pattern;
wenzelm [Sun, 07 May 2006 00:44:50 +0200] rev 19586
removed 'concl is' pattern;
Sun, 07 May 2006 00:22:05 +0200 removed 'concl is' patterns;
wenzelm [Sun, 07 May 2006 00:22:05 +0200] rev 19585
removed 'concl is' patterns;
Sun, 07 May 2006 00:21:13 +0200 tuned;
wenzelm [Sun, 07 May 2006 00:21:13 +0200] rev 19584
tuned;
Sun, 07 May 2006 00:00:13 +0200 function-package: Changed record usage to make sml/nj happy...
krauss [Sun, 07 May 2006 00:00:13 +0200] rev 19583
function-package: Changed record usage to make sml/nj happy...
Fri, 05 May 2006 22:11:19 +0200 get rid of 'concl is';
wenzelm [Fri, 05 May 2006 22:11:19 +0200] rev 19582
get rid of 'concl is';
Fri, 05 May 2006 21:59:49 +0200 more robust pretty_term_typ, using well-typed parse tree representation;
wenzelm [Fri, 05 May 2006 21:59:49 +0200] rev 19581
more robust pretty_term_typ, using well-typed parse tree representation;
Fri, 05 May 2006 21:59:48 +0200 replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm [Fri, 05 May 2006 21:59:48 +0200] rev 19580
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
Fri, 05 May 2006 21:59:47 +0200 replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
wenzelm [Fri, 05 May 2006 21:59:47 +0200] rev 19579
replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR; add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;
Fri, 05 May 2006 21:59:46 +0200 added class_error and exception CLASS_ERROR (supercedes DOMAIN);
wenzelm [Fri, 05 May 2006 21:59:46 +0200] rev 19578
added class_error and exception CLASS_ERROR (supercedes DOMAIN); clarified of_class_derivation; tuned witness_sorts;
Fri, 05 May 2006 21:59:45 +0200 added syntax for _type_constraint_;
wenzelm [Fri, 05 May 2006 21:59:45 +0200] rev 19577
added syntax for _type_constraint_;
Fri, 05 May 2006 21:59:44 +0200 extern_early: improved handling of undeclared constants;
wenzelm [Fri, 05 May 2006 21:59:44 +0200] rev 19576
extern_early: improved handling of undeclared constants;
Fri, 05 May 2006 21:59:43 +0200 replaced Graph.find_paths by Graph.irreducible_paths;
wenzelm [Fri, 05 May 2006 21:59:43 +0200] rev 19575
replaced Graph.find_paths by Graph.irreducible_paths;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip