wenzelm [Thu, 14 Feb 2002 20:30:49 +0100] rev 12890
made MLWorks happy;
nipkow [Thu, 14 Feb 2002 12:24:02 +0100] rev 12889
*** empty log message ***
nipkow [Thu, 14 Feb 2002 12:06:07 +0100] rev 12888
nodups -> distinct
nipkow [Thu, 14 Feb 2002 11:50:52 +0100] rev 12887
nodups -> distinct
paulson [Wed, 13 Feb 2002 10:48:29 +0100] rev 12886
deleted some redundant 'addS*Es [equalityC*E]'s
paulson [Wed, 13 Feb 2002 10:45:08 +0100] rev 12885
new function lemmas
paulson [Wed, 13 Feb 2002 10:44:39 +0100] rev 12884
tidied. no more special simpset (super_ss)
paulson [Wed, 13 Feb 2002 10:44:07 +0100] rev 12883
new lemmas for closure under Union
wenzelm [Tue, 12 Feb 2002 20:35:35 +0100] rev 12882
eliminated Pure/Isar/comment.ML;
wenzelm [Tue, 12 Feb 2002 20:34:02 +0100] rev 12881
ANTIQUOTE_FAIL;
wenzelm [Tue, 12 Feb 2002 20:33:37 +0100] rev 12880
eliminated Isar/comment.ML;
wenzelm [Tue, 12 Feb 2002 20:33:03 +0100] rev 12879
tuned;
wenzelm [Tue, 12 Feb 2002 20:32:23 +0100] rev 12878
added isabelle-hol-book;
added tphols2001;
tuned tphols2000;
wenzelm [Tue, 12 Feb 2002 20:31:40 +0100] rev 12877
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
wenzelm [Tue, 12 Feb 2002 20:28:27 +0100] rev 12876
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm [Tue, 12 Feb 2002 20:25:58 +0100] rev 12875
tuned;
wenzelm [Mon, 11 Feb 2002 17:30:58 +0100] rev 12874
ML-Systems/smlnj-compiler.ML compatibility tweak;
wenzelm [Mon, 11 Feb 2002 10:56:33 +0100] rev 12873
include SVC_Test;
berghofe [Thu, 07 Feb 2002 11:07:03 +0100] rev 12872
Theorems are only "pre-named" if the do not already have names.
berghofe [Wed, 06 Feb 2002 14:10:35 +0100] rev 12871
Added function could_unify to speed up rewriting of proof terms.
berghofe [Wed, 06 Feb 2002 14:09:55 +0100] rev 12870
Indexes of variables in expanded proofs are now incremented to avoid clashes.
wenzelm [Tue, 05 Feb 2002 23:18:08 +0100] rev 12869
moved SVC stuff to ex;
berghofe [Tue, 05 Feb 2002 15:51:28 +0100] rev 12868
New function maxidx_of_proof.
paulson [Mon, 04 Feb 2002 13:16:54 +0100] rev 12867
New-style versions of these old examples
berghofe [Sat, 02 Feb 2002 13:26:51 +0100] rev 12866
Rewrite procedure now works for both compact and full proof objects.
wenzelm [Wed, 30 Jan 2002 14:05:29 +0100] rev 12865
escape_mfix;
wenzelm [Wed, 30 Jan 2002 14:00:36 +0100] rev 12864
added literal;
wenzelm [Wed, 30 Jan 2002 14:00:25 +0100] rev 12863
prep_mixfix': proper use of Syntax.literal;
wenzelm [Wed, 30 Jan 2002 13:59:57 +0100] rev 12862
tuned;
paulson [Wed, 30 Jan 2002 12:22:59 +0100] rev 12861
mu-syntax for the LEAST operator
paulson [Wed, 30 Jan 2002 12:22:40 +0100] rev 12860
Multiset: added the translation Mult(A) => A-||>nat-{0}
(which internalises the `multiset' relation).
FoldSet: weakened the typing conditions of the function f and
(by the way) removed the `locale' declarations.
wenzelm [Mon, 28 Jan 2002 23:35:20 +0100] rev 12859
tuned;
wenzelm [Mon, 28 Jan 2002 18:51:48 +0100] rev 12858
GPLed;
wenzelm [Mon, 28 Jan 2002 18:50:23 +0100] rev 12857
tuned header;
wenzelm [Mon, 28 Jan 2002 18:48:25 +0100] rev 12856
tuned;
schirmer [Mon, 28 Jan 2002 17:52:13 +0100] rev 12855
Bali added
schirmer [Mon, 28 Jan 2002 17:00:19 +0100] rev 12854
Isabelle/Bali sources;
wenzelm [Sat, 26 Jan 2002 19:20:01 +0100] rev 12853
Isar cases/induct: no backtracking;
wenzelm [Sat, 26 Jan 2002 19:17:15 +0100] rev 12852
cases: really append cases_default;
cases/induct method: DETERM;
wenzelm [Sat, 26 Jan 2002 19:15:51 +0100] rev 12851
generic DETERM;
paulson [Fri, 25 Jan 2002 15:42:59 +0100] rev 12850
ZF
wenzelm [Thu, 24 Jan 2002 22:44:10 +0100] rev 12849
copy_files *.sty;
wenzelm [Thu, 24 Jan 2002 22:43:40 +0100] rev 12848
cond_print_result_rule: priority (again) instead of slightly
ill-behaved tracing output;
wenzelm [Thu, 24 Jan 2002 22:42:14 +0100] rev 12847
fixed subgoal_tac; fails on non-existent subgoal;
wenzelm [Thu, 24 Jan 2002 22:41:44 +0100] rev 12846
copy_styles replaces overly conservative update_styles;
wenzelm [Thu, 24 Jan 2002 18:22:01 +0100] rev 12845
Springer LNCS 2283;
wenzelm [Thu, 24 Jan 2002 16:37:49 +0100] rev 12844
updated;
wenzelm [Thu, 24 Jan 2002 16:37:43 +0100] rev 12843
iff del: less_Suc0 -- luckily this does NOT affect the printed text;
wenzelm [Wed, 23 Jan 2002 17:13:54 +0100] rev 12842
delsimps [less_Suc0];
wenzelm [Wed, 23 Jan 2002 17:01:53 +0100] rev 12841
less_Suc0;
wenzelm [Wed, 23 Jan 2002 16:58:45 +0100] rev 12840
error "Unexpected end of input";
wenzelm [Wed, 23 Jan 2002 16:58:26 +0100] rev 12839
reorganized code for predicate text;
wenzelm [Wed, 23 Jan 2002 16:58:05 +0100] rev 12838
tuned;
lemmas nat_number_of;
wenzelm [Wed, 23 Jan 2002 16:57:33 +0100] rev 12837
* HOL: nat_number_of;
paulson [Wed, 23 Jan 2002 11:43:53 +0100] rev 12836
A few more standard simprules, TCs, etc.
wenzelm [Tue, 22 Jan 2002 21:19:15 +0100] rev 12835
qualified_result replaces qualified;
wenzelm [Tue, 22 Jan 2002 21:18:36 +0100] rev 12834
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm [Mon, 21 Jan 2002 22:27:34 +0100] rev 12833
full_proofs;
wenzelm [Mon, 21 Jan 2002 17:03:38 +0100] rev 12832
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
wenzelm [Mon, 21 Jan 2002 17:02:52 +0100] rev 12831
reset show_hyps by default (in accordance to existing Isar practice);
wenzelm [Mon, 21 Jan 2002 16:28:22 +0100] rev 12830
save library;
wenzelm [Mon, 21 Jan 2002 16:15:16 +0100] rev 12829
full_atomize;
wenzelm [Mon, 21 Jan 2002 15:29:06 +0100] rev 12828
wild guess at polyml-4.1.2;
wenzelm [Mon, 21 Jan 2002 15:28:34 +0100] rev 12827
options -l and -t;
tuned;
berghofe [Mon, 21 Jan 2002 14:48:11 +0100] rev 12826
Removed timing function.
paulson [Mon, 21 Jan 2002 14:47:55 +0100] rev 12825
new simprules and classical rules
berghofe [Mon, 21 Jan 2002 14:47:47 +0100] rev 12824
Tuned name mangling function.
berghofe [Mon, 21 Jan 2002 14:45:00 +0100] rev 12823
Made some proofs constructive.
berghofe [Mon, 21 Jan 2002 14:43:38 +0100] rev 12822
datatype_codegen now checks type of constructor.
nipkow [Mon, 21 Jan 2002 13:44:16 +0100] rev 12821
*** empty log message ***
paulson [Mon, 21 Jan 2002 11:25:45 +0100] rev 12820
lexical tidying
paulson [Mon, 21 Jan 2002 10:52:05 +0100] rev 12819
slight re-use of code
kleing [Sat, 19 Jan 2002 15:44:53 +0100] rev 12818
fixed typos
wenzelm [Fri, 18 Jan 2002 18:36:19 +0100] rev 12817
rewrite_term: removed rew0, so no on-the-fly eta-contraction;
wenzelm [Fri, 18 Jan 2002 18:35:39 +0100] rev 12816
fixed document setup of HOL-Library;
wenzelm [Fri, 18 Jan 2002 18:30:19 +0100] rev 12815
tuned;
paulson [Fri, 18 Jan 2002 17:46:17 +0100] rev 12814
tidied
paulson [Fri, 18 Jan 2002 17:45:19 +0100] rev 12813
OOPS
paulson [Fri, 18 Jan 2002 17:44:15 +0100] rev 12812
tweaks
wenzelm [Fri, 18 Jan 2002 15:17:47 +0100] rev 12811
moved document sources to proper place, *within* Library/Library (!);
wenzelm [Thu, 17 Jan 2002 21:07:11 +0100] rev 12810
cover polyml-4.1.2;
wenzelm [Thu, 17 Jan 2002 21:07:00 +0100] rev 12809
RuleCases.make interface based on term instead of thm;
wenzelm [Thu, 17 Jan 2002 21:06:23 +0100] rev 12808
RuleCases.make interface based on term instead of thm;
tuned;
wenzelm [Thu, 17 Jan 2002 21:05:58 +0100] rev 12807
atomize_term replaces atomize_cterm;
wenzelm [Thu, 17 Jan 2002 21:05:40 +0100] rev 12806
ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;
wenzelm [Thu, 17 Jan 2002 21:04:48 +0100] rev 12805
Thm.prop_of;
wenzelm [Thu, 17 Jan 2002 21:04:36 +0100] rev 12804
Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
wenzelm [Thu, 17 Jan 2002 21:04:16 +0100] rev 12803
added prop_of: thm -> term (at last!);
wenzelm [Thu, 17 Jan 2002 21:03:55 +0100] rev 12802
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm [Thu, 17 Jan 2002 21:03:29 +0100] rev 12801
renamed norm_hhf to norm_hhf_rule;
removed slow rewrite_cterm;
wenzelm [Thu, 17 Jan 2002 21:02:52 +0100] rev 12800
added is_norm_hhf (from logic.ML);
norm_hhf based on fast Pattern.rewrite_term;
wenzelm [Thu, 17 Jan 2002 21:02:18 +0100] rev 12799
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
RuleCases.make interface based on term instead of thm;
wenzelm [Thu, 17 Jan 2002 21:01:17 +0100] rev 12798
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm [Thu, 17 Jan 2002 21:00:38 +0100] rev 12797
eta_contract with sharing (by berghofe);
rewrite_term: proper handling of Abs cong;
wenzelm [Thu, 17 Jan 2002 20:59:46 +0100] rev 12796
is_norm_hhf moved to drule.ML;
wenzelm [Thu, 17 Jan 2002 20:59:31 +0100] rev 12795
added timeap_msg;
nipkow [Thu, 17 Jan 2002 19:37:57 +0100] rev 12794
new style theory
nipkow [Thu, 17 Jan 2002 19:37:42 +0100] rev 12793
Lex dependencies modified
nipkow [Thu, 17 Jan 2002 19:32:22 +0100] rev 12792
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
kleing [Thu, 17 Jan 2002 15:06:36 +0100] rev 12791
registered directly executable version with the code generator
nipkow [Thu, 17 Jan 2002 12:58:31 +0100] rev 12790
*** empty log message ***
paulson [Thu, 17 Jan 2002 12:45:52 +0100] rev 12789
new definitions from Sidi Ehmety
paulson [Thu, 17 Jan 2002 12:45:36 +0100] rev 12788
made proofs more robust
paulson [Thu, 17 Jan 2002 10:35:59 +0100] rev 12787
mistakenly deleted this theory
kleing [Thu, 17 Jan 2002 09:01:10 +0100] rev 12786
fixed
wenzelm [Wed, 16 Jan 2002 23:19:34 +0100] rev 12785
GPLed;
wenzelm [Wed, 16 Jan 2002 23:18:20 +0100] rev 12784
added rewrite_term;
tuned;
GPLed;
wenzelm [Wed, 16 Jan 2002 23:17:44 +0100] rev 12783
interface to Pattern.rewrite_term;
wenzelm [Wed, 16 Jan 2002 22:24:37 +0100] rev 12782
tune norm_hhf_tac;
wenzelm [Wed, 16 Jan 2002 22:23:46 +0100] rev 12781
added beta_eta_contract;
wenzelm [Wed, 16 Jan 2002 21:01:08 +0100] rev 12780
tuned title;
wenzelm [Wed, 16 Jan 2002 20:58:27 +0100] rev 12779
export beta_eta_conversion;
wenzelm [Wed, 16 Jan 2002 20:57:02 +0100] rev 12778
Interface/proof_general.ML move to proof_general.ML;
paulson [Wed, 16 Jan 2002 17:53:22 +0100] rev 12777
Isar version of ZF/AC
paulson [Wed, 16 Jan 2002 17:52:06 +0100] rev 12776
Isar version of AC
wenzelm [Wed, 16 Jan 2002 15:04:37 +0100] rev 12775
norm_hhf;
kleing [Tue, 15 Jan 2002 23:23:09 +0100] rev 12774
fixed theory deps
kleing [Tue, 15 Jan 2002 22:22:05 +0100] rev 12773
use exec_lub instead of some_lub
kleing [Tue, 15 Jan 2002 22:21:30 +0100] rev 12772
tuned for directly executable definitions
wenzelm [Tue, 15 Jan 2002 21:09:31 +0100] rev 12771
tuned;