nipkow [Fri, 30 Jun 2006 18:26:22 +0200] rev 19970
normalization uses refl now
mengj [Fri, 30 Jun 2006 12:22:29 +0200] rev 19969
Removed some incorrect axioms.
haftmann [Fri, 30 Jun 2006 12:04:17 +0200] rev 19968
fixed stale theory bug
haftmann [Fri, 30 Jun 2006 12:04:03 +0200] rev 19967
slight refinements
haftmann [Fri, 30 Jun 2006 12:03:36 +0200] rev 19966
refinement in instance command
haftmann [Fri, 30 Jun 2006 12:03:21 +0200] rev 19965
small change in class_package
paulson [Thu, 29 Jun 2006 18:11:15 +0200] rev 19964
added the "th" field to datatype Clause
paulson [Thu, 29 Jun 2006 18:10:59 +0200] rev 19963
fixed the "factor" method
nipkow [Thu, 29 Jun 2006 13:53:05 +0200] rev 19962
new function norm_term
nipkow [Thu, 29 Jun 2006 13:52:28 +0200] rev 19961
new method "normalization"
kleing [Thu, 29 Jun 2006 01:08:08 +0200] rev 19960
use -f in cp to overwrite read-only files (e.g. .svn in document/)
webertj [Wed, 28 Jun 2006 17:54:00 +0200] rev 19959
world map now transparent
haftmann [Wed, 28 Jun 2006 14:36:47 +0200] rev 19958
improvements in Classpackage
haftmann [Wed, 28 Jun 2006 14:36:09 +0200] rev 19957
reduced code, better instance command
haftmann [Wed, 28 Jun 2006 14:35:51 +0200] rev 19956
slight improvements in code generation
haftmann [Wed, 28 Jun 2006 14:35:10 +0200] rev 19955
added lookup function for parameters
paulson [Wed, 28 Jun 2006 09:27:53 +0200] rev 19954
disjunctive wellfoundedness
haftmann [Tue, 27 Jun 2006 10:10:20 +0200] rev 19953
class package refinements, slight code generation refinements
haftmann [Tue, 27 Jun 2006 10:09:48 +0200] rev 19952
added class projection
haftmann [Tue, 27 Jun 2006 10:09:44 +0200] rev 19951
slight improvement
haftmann [Tue, 27 Jun 2006 10:09:39 +0200] rev 19950
replaced subgraph by project
wenzelm [Sat, 24 Jun 2006 22:54:37 +0200] rev 19949
fix/fixes: tuned type constraints;
wenzelm [Sat, 24 Jun 2006 22:25:31 +0200] rev 19948
minor tuning of definitions/proofs;
wenzelm [Sat, 24 Jun 2006 22:25:30 +0200] rev 19947
fixed translations for _MapUpd: CONST;
nipkow [Fri, 23 Jun 2006 13:42:19 +0200] rev 19946
beautification
haftmann [Fri, 23 Jun 2006 10:48:34 +0200] rev 19945
added webmaster
paulson [Fri, 23 Jun 2006 09:55:01 +0200] rev 19944
Introduction of Ramsey's theorem
ballarin [Thu, 22 Jun 2006 18:48:25 +0200] rev 19943
Removed debugging code.
ballarin [Thu, 22 Jun 2006 07:08:04 +0200] rev 19942
Improved handling of defines imported in duplicate.
kleing [Thu, 22 Jun 2006 05:16:15 +0200] rev 19941
new standard dir structure
webertj [Wed, 21 Jun 2006 21:30:57 +0200] rev 19940
world map updated
webertj [Wed, 21 Jun 2006 21:13:27 +0200] rev 19939
world map updated
krauss [Wed, 21 Jun 2006 11:44:50 +0200] rev 19938
Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
haftmann [Wed, 21 Jun 2006 11:24:19 +0200] rev 19937
fixed bug resolving Haskell names
haftmann [Wed, 21 Jun 2006 11:23:49 +0200] rev 19936
fixed error bug
haftmann [Wed, 21 Jun 2006 11:23:06 +0200] rev 19935
renamed thy data
krauss [Wed, 21 Jun 2006 11:08:04 +0200] rev 19934
Added split_cong rule
haftmann [Wed, 21 Jun 2006 10:26:39 +0200] rev 19933
hyps better than prems
haftmann [Tue, 20 Jun 2006 16:46:30 +0200] rev 19932
fixed sml/nj value restriction problem
ballarin [Tue, 20 Jun 2006 15:53:44 +0200] rev 19931
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
krauss [Tue, 20 Jun 2006 14:51:59 +0200] rev 19930
Fixed another variable order bug...
haftmann [Tue, 20 Jun 2006 10:16:22 +0200] rev 19929
switched to open locales for classes
haftmann [Tue, 20 Jun 2006 10:10:06 +0200] rev 19928
switched to open locales for classes
wenzelm [Mon, 19 Jun 2006 22:06:36 +0200] rev 19927
refrain from reforming TFL -- back to previous revision;
wenzelm [Mon, 19 Jun 2006 20:21:32 +0200] rev 19926
added declare_thm, thm_context;
added trade(T);
wenzelm [Mon, 19 Jun 2006 20:21:30 +0200] rev 19925
eliminated freeze/varify in favour of Variable.import/export/trade;
webertj [Mon, 19 Jun 2006 19:56:32 +0200] rev 19924
world map updated
webertj [Mon, 19 Jun 2006 19:17:48 +0200] rev 19923
world map updated
krauss [Mon, 19 Jun 2006 18:25:34 +0200] rev 19922
Fixed name clash.
Function-goals are now fully quantified.
Avoiding large meta-conjunctions when setting up the goal.
Cleanup.
webertj [Mon, 19 Jun 2006 18:02:49 +0200] rev 19921
world map updated
wenzelm [Mon, 19 Jun 2006 17:19:04 +0200] rev 19920
matchers: try pattern_matchers only *after* general matching (The
pattern version is not a faithful approximation because it falls back
on first-order matching!);
wenzelm [Sat, 17 Jun 2006 19:38:01 +0200] rev 19919
ProofContext.exports: simultaneous facts;
wenzelm [Sat, 17 Jun 2006 19:38:00 +0200] rev 19918
moved internal/skolem to term.ML;
wenzelm [Sat, 17 Jun 2006 19:37:59 +0200] rev 19917
mutual_rule: proper context;
wenzelm [Sat, 17 Jun 2006 19:37:58 +0200] rev 19916
export: simultaneous facts, refer to Variable.export;
Term.internal/skolem;
wenzelm [Sat, 17 Jun 2006 19:37:57 +0200] rev 19915
ProofContext.exports: simultaneous facts;
Variable.exportT_terms;
wenzelm [Sat, 17 Jun 2006 19:37:55 +0200] rev 19914
Variable.importT_inst;
Term.internal;
wenzelm [Sat, 17 Jun 2006 19:37:54 +0200] rev 19913
standard: simultaneous facts;
wenzelm [Sat, 17 Jun 2006 19:37:53 +0200] rev 19912
added singleton;
wenzelm [Sat, 17 Jun 2006 19:37:52 +0200] rev 19911
major reworking of export functionality -- based on Term/Thm.generalize;
tuned interfaces;
wenzelm [Sat, 17 Jun 2006 19:37:51 +0200] rev 19910
added generalize rule;
added maxidx_thm;
wenzelm [Sat, 17 Jun 2006 19:37:50 +0200] rev 19909
added exists_subtype;
added internal/skolem (from Syntax/lexicon.ML);
added generalize(T);
wenzelm [Sat, 17 Jun 2006 19:37:49 +0200] rev 19908
added generalize rule;
wenzelm [Sat, 17 Jun 2006 19:37:48 +0200] rev 19907
Term.skolem;
wenzelm [Sat, 17 Jun 2006 19:37:47 +0200] rev 19906
Term.internal;
wenzelm [Sat, 17 Jun 2006 19:37:46 +0200] rev 19905
ProofContext.export: singleton;
wenzelm [Sat, 17 Jun 2006 19:37:45 +0200] rev 19904
RuleCases.mutual_rule: ctxt;
ProofContext.exports: simultaneous facts;
wenzelm [Sat, 17 Jun 2006 19:37:43 +0200] rev 19903
RuleCases.mutual_rule: ctxt;
Term.internal;
ProofContext.exports: simultaneous facts;
dixon [Sat, 17 Jun 2006 18:58:12 +0200] rev 19902
added interface for making term contexts.
haftmann [Fri, 16 Jun 2006 09:08:34 +0200] rev 19901
fixed symlink bug
wenzelm [Thu, 15 Jun 2006 23:10:45 +0200] rev 19900
ProofContext: moved variable operations to struct Variable;
tuned;
wenzelm [Thu, 15 Jun 2006 23:08:58 +0200] rev 19899
Fixed type/term variables and polymorphic term abbreviations.
wenzelm [Thu, 15 Jun 2006 23:08:56 +0200] rev 19898
added variable.ML;
wenzelm [Thu, 15 Jun 2006 23:08:54 +0200] rev 19897
ProofContext: moved variable operations to struct Variable;
nipkow [Thu, 15 Jun 2006 18:35:16 +0200] rev 19896
*** empty log message ***
nipkow [Thu, 15 Jun 2006 18:28:32 +0200] rev 19895
*** empty log message ***
paulson [Thu, 15 Jun 2006 17:50:47 +0200] rev 19894
the "all_theorems" option and some fixes
paulson [Thu, 15 Jun 2006 17:50:30 +0200] rev 19893
the enumerate operator
webertj [Wed, 14 Jun 2006 16:18:10 +0200] rev 19892
Jia Meng added to world map
haftmann [Wed, 14 Jun 2006 12:16:49 +0200] rev 19891
keyword update
haftmann [Wed, 14 Jun 2006 12:14:42 +0200] rev 19890
slight adaption for code generator
haftmann [Wed, 14 Jun 2006 12:14:13 +0200] rev 19889
slight adaptions for code generator
haftmann [Wed, 14 Jun 2006 12:13:12 +0200] rev 19888
slight adaptions
haftmann [Wed, 14 Jun 2006 12:12:37 +0200] rev 19887
slight refinements for code generator
haftmann [Wed, 14 Jun 2006 12:12:01 +0200] rev 19886
added hook for case const defs
haftmann [Wed, 14 Jun 2006 12:11:23 +0200] rev 19885
added codegen_simtype
haftmann [Wed, 14 Jun 2006 12:10:57 +0200] rev 19884
improvements in code generator
wenzelm [Tue, 13 Jun 2006 23:41:59 +0200] rev 19883
avoid global Drule.unvarify;
wenzelm [Tue, 13 Jun 2006 23:41:58 +0200] rev 19882
tuned interfaces;
added invent_types;
added import_types/terms;
wenzelm [Tue, 13 Jun 2006 23:41:52 +0200] rev 19881
added hyps_of;
tuned;
wenzelm [Tue, 13 Jun 2006 23:41:49 +0200] rev 19880
added equiv;
wenzelm [Tue, 13 Jun 2006 23:41:47 +0200] rev 19879
(un)varify: tuned exceptions;
wenzelm [Tue, 13 Jun 2006 23:41:44 +0200] rev 19878
removed weak_eq_thm;
added equiv_thm;
removed obsolete unvarifyT;
improved unvarify -- demands global context (cf. Logic.unvarify);
wenzelm [Tue, 13 Jun 2006 23:41:41 +0200] rev 19877
Drule.equiv_thm supercedes Drule.weak_eq_thm;
wenzelm [Tue, 13 Jun 2006 23:41:39 +0200] rev 19876
tuned;
wenzelm [Tue, 13 Jun 2006 23:41:37 +0200] rev 19875
avoid unqualified exception names;
tuned;
wenzelm [Tue, 13 Jun 2006 23:41:34 +0200] rev 19874
ProjectRule now context dependent;
wenzelm [Tue, 13 Jun 2006 23:41:31 +0200] rev 19873
use Drule.unvarify instead of obsolete Drule.freeze_all;
dixon [Tue, 13 Jun 2006 15:42:52 +0200] rev 19872
corrected w.r.t. search order for subst.
dixon [Tue, 13 Jun 2006 15:42:19 +0200] rev 19871
Corrected search order for zippers.
paulson [Tue, 13 Jun 2006 15:07:58 +0200] rev 19870
new results
paulson [Tue, 13 Jun 2006 15:07:47 +0200] rev 19869
removal of the obsolete "infinite_nonempty"
wenzelm [Mon, 12 Jun 2006 22:14:38 +0200] rev 19868
tuned;
wenzelm [Mon, 12 Jun 2006 21:19:07 +0200] rev 19867
added declare_typ;
simult_matches: Unify.matchers;
wenzelm [Mon, 12 Jun 2006 21:19:06 +0200] rev 19866
tuned;
wenzelm [Mon, 12 Jun 2006 21:19:05 +0200] rev 19865
tuned interfaces;
wenzelm [Mon, 12 Jun 2006 21:19:04 +0200] rev 19864
added matchers, matches_list;
tuned interfaces;
wenzelm [Mon, 12 Jun 2006 21:19:03 +0200] rev 19863
removed matches_seq -- didn't quite work;
wenzelm [Mon, 12 Jun 2006 21:19:02 +0200] rev 19862
Unify.matches_list;
wenzelm [Mon, 12 Jun 2006 21:19:00 +0200] rev 19861
tuned Seq/Envir/Unify interfaces;
wenzelm [Mon, 12 Jun 2006 21:18:10 +0200] rev 19860
fixed subst step;
wenzelm [Mon, 12 Jun 2006 20:58:25 +0200] rev 19859
avoid accidental binding of ?Jmp;
urbanc [Mon, 12 Jun 2006 20:32:33 +0200] rev 19858
added lemma fresh_unit to Nominal.thy
made the fresh_guess tactic to solve more goals
adapted Iteration.thy to use the new tactic
berghofe [Mon, 12 Jun 2006 18:17:21 +0200] rev 19857
Added fresh_guess_tac.
berghofe [Mon, 12 Jun 2006 18:15:45 +0200] rev 19856
Removed comments around declaration of fresh_guess method.
berghofe [Mon, 12 Jun 2006 17:16:03 +0200] rev 19855
Added "evaluation" method.
haftmann [Mon, 12 Jun 2006 15:58:12 +0200] rev 19854
updated keywords
wenzelm [Mon, 12 Jun 2006 11:59:25 +0200] rev 19853
made smlnj happy;
haftmann [Mon, 12 Jun 2006 09:14:41 +0200] rev 19852
fixed smlnj incompat.
berghofe [Mon, 12 Jun 2006 00:36:52 +0200] rev 19851
Completely rewrote code for defining graph of recursion combinator.