wenzelm [Tue, 04 Jul 2006 21:22:51 +0200] rev 20010
added props selector;
wenzelm [Tue, 04 Jul 2006 21:22:50 +0200] rev 20009
print_facts: all facts;
wenzelm [Tue, 04 Jul 2006 19:49:59 +0200] rev 20008
add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;
wenzelm [Tue, 04 Jul 2006 19:49:58 +0200] rev 20007
instantiate_tfrees: Thm.generalize;
wenzelm [Tue, 04 Jul 2006 19:49:57 +0200] rev 20006
removed parrot comment;
wenzelm [Tue, 04 Jul 2006 19:49:56 +0200] rev 20005
Proof by guessing.
wenzelm [Tue, 04 Jul 2006 19:49:55 +0200] rev 20004
guess: proper context for polymorphic parameters;
tuned;
wenzelm [Tue, 04 Jul 2006 19:49:54 +0200] rev 20003
polymorphic: always generalize wrt. used_types;
wenzelm [Tue, 04 Jul 2006 19:49:53 +0200] rev 20002
varifyT: no longer pervasive;
wenzelm [Tue, 04 Jul 2006 19:49:52 +0200] rev 20001
added generalize/instantiate_option;
wenzelm [Tue, 04 Jul 2006 19:49:51 +0200] rev 20000
added map_proof_terms_option;
tuned generalize, instantiate;
wenzelm [Tue, 04 Jul 2006 19:49:50 +0200] rev 19999
added generalize;
removed obsolete assume_ax, tvars_intr_list;
wenzelm [Tue, 04 Jul 2006 19:49:49 +0200] rev 19998
Thm.varifyT;
wenzelm [Tue, 04 Jul 2006 19:49:47 +0200] rev 19997
added ex/Guess.thy;
wenzelm [Tue, 04 Jul 2006 18:39:59 +0200] rev 19996
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm [Tue, 04 Jul 2006 18:39:58 +0200] rev 19995
added schematic_goal;
wenzelm [Tue, 04 Jul 2006 18:39:57 +0200] rev 19994
added 'unfolding';
urbanc [Tue, 04 Jul 2006 17:26:02 +0200] rev 19993
added simplification rules to the fresh_guess tactic
urbanc [Tue, 04 Jul 2006 15:57:19 +0200] rev 19992
made calc_atm stronger by including some relative
obvious simplification rules
ballarin [Tue, 04 Jul 2006 15:45:59 +0200] rev 19991
Locales no longer generate views. The following functions have changed
signatures: Locale.init, Locale.add_thmss, Locale.read/cert_context_statement.
wenzelm [Tue, 04 Jul 2006 15:30:30 +0200] rev 19990
added 'definition', 'unfolding', 'done';
tuned;
wenzelm [Tue, 04 Jul 2006 15:30:29 +0200] rev 19989
tuned;
wenzelm [Tue, 04 Jul 2006 15:30:28 +0200] rev 19988
added 'value';
tuned;
berghofe [Tue, 04 Jul 2006 15:26:56 +0200] rev 19987
- put declarations inside a structure (NominalPermeq)
- dynamic_thm(s) now looks up theorems in theory
associated with proof state (rather than in context
associated with simpset)
- finite_guess_tac now automatically adds some extra
rules about supp to the simpset
berghofe [Tue, 04 Jul 2006 15:22:54 +0200] rev 19986
- nominal_permeq.ML is now loaded before nominal_package.ML
- methods and tactics in nominal_permeq.ML are now defined
inside structure NominalPermeq, therefore the names
in the method_setup section had to be changed
berghofe [Tue, 04 Jul 2006 15:20:43 +0200] rev 19985
Implemented proofs of equivariance and finite support
for graph of recursion combinator.
ballarin [Tue, 04 Jul 2006 14:47:01 +0200] rev 19984
Method intro_locales replaced by intro_locales and unfold_locales.
urbanc [Tue, 04 Jul 2006 12:13:38 +0200] rev 19983
updated
ballarin [Tue, 04 Jul 2006 11:36:08 +0200] rev 19982
Typo.
ballarin [Tue, 04 Jul 2006 11:35:49 +0200] rev 19981
Minor new lemmas.
nipkow [Mon, 03 Jul 2006 20:03:11 +0200] rev 19980
replaced respects2 by congruent2 because of type problem
nipkow [Mon, 03 Jul 2006 20:02:42 +0200] rev 19979
replaced translation by abbreviation
wenzelm [Mon, 03 Jul 2006 19:33:09 +0200] rev 19978
obtain_export: Thm.generalize;
guess: fixed handling of mixfixes of vars;
tuned;
wenzelm [Mon, 03 Jul 2006 19:33:07 +0200] rev 19977
project_algebra: norm_sort;
tuned;
webertj [Mon, 03 Jul 2006 17:27:09 +0200] rev 19976
comments fixed, minor optimization wrt. certifying terms
dixon [Mon, 03 Jul 2006 17:24:45 +0200] rev 19975
fix to subst in order to allow subst when head of a term is a bound variable.
webertj [Mon, 03 Jul 2006 17:17:41 +0200] rev 19974
CNF tactic invocations moved into comments
webertj [Mon, 03 Jul 2006 16:25:10 +0200] rev 19973
comment added
urbanc [Sun, 02 Jul 2006 17:27:10 +0200] rev 19972
added more infrastructure for the recursion combinator
nipkow [Fri, 30 Jun 2006 18:26:36 +0200] rev 19971
normal_form to lemma test
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;