| 2007-04-15 |
wenzelm |
proper interface infer_types(_pat);
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
Thm.fold_terms;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
removed unused Output.panic hook -- internal to PG wrapper;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
moved get_sort to sign.ML;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
removed obsolete inferT_axm;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
removed obsolete infer_types(_simult);
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
load type_infer.ML early;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
adapted decode_type;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
proper ProofContext.infer_types;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
Thm.fold_terms;
|
changeset |
files
|
| 2007-04-15 |
wenzelm |
replaced axioms/finalconsts by proper axiomatization;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
simplified read_axm;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
tuned comment;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
removed redundant string_of_vname (see term.ML);
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
removed obsolete read_ctyp, read_def_cterm;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
read_typ_XXX: no sorts;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
added read_def_cterms, read_cterm (from thm.ML);
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
removed Pure/Syntax/ROOT.ML;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
Term.string_of_vname;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
Theory.inferT_axm;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
do not enable Toplevel.debug globally;
|
changeset |
files
|
| 2007-04-14 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| 2007-04-14 |
haftmann |
canonical merge operations
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
declarations: apply target_morphism;
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
inst(T)_morphism: avoid reference to static theory value;
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
added Morphism.transform/form (generic non-sense);
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
Morphism.transform/form;
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
data declaration: removed obsolete target_morphism (still required for local data!?);
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
data declaration: removed obsolete target_morphism;
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
added eval_antiquotes_fn (tmp);
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
tuned document (headers, sections, spacing);
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
do translation: CONST;
|
changeset |
files
|
| 2007-04-13 |
wenzelm |
eval_antiquotes: proper parentheses for projection;
|
changeset |
files
|
| 2007-04-13 |
haftmann |
canonical merge operations
|
changeset |
files
|
| 2007-04-13 |
berghofe |
Removed erroneous application of rev in get_clauses that caused
|
changeset |
files
|
| 2007-04-13 |
krauss |
more robust proof
|
changeset |
files
|
| 2007-04-13 |
ballarin |
Experimental code for the interpretation of definitions.
|
changeset |
files
|
| 2007-04-13 |
ballarin |
Experimental interpretation code for definitions.
|
changeset |
files
|
| 2007-04-13 |
ballarin |
New file for locale regression tests.
|
changeset |
files
|
| 2007-04-13 |
narboux |
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
|
changeset |
files
|
| 2007-04-12 |
huffman |
minimize imports
|
changeset |
files
|
| 2007-04-12 |
huffman |
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
|
changeset |
files
|
| 2007-04-12 |
huffman |
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
|
changeset |
files
|
| 2007-04-12 |
wenzelm |
added proj_value_antiq;
|
changeset |
files
|
| 2007-04-12 |
wenzelm |
absdummy: use internal name uu to avoid renaming of popular names;
|
changeset |
files
|
| 2007-04-12 |
urbanc |
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
|
changeset |
files
|
| 2007-04-12 |
wenzelm |
updated;
|
changeset |
files
|
| 2007-04-12 |
wenzelm |
output_basic: added isaantiq markup (only inside verbatim tokens);
|
changeset |
files
|
| 2007-04-12 |
wenzelm |
newenvironment{isaantiq};
|
changeset |
files
|
| 2007-04-12 |
paulson |
Zero variable indexes in clauses
|
changeset |
files
|
| 2007-04-12 |
paulson |
Improved treatment of classrel/arity clauses
|
changeset |
files
|
| 2007-04-12 |
paulson |
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
|
changeset |
files
|
| 2007-04-12 |
paulson |
Improved and simplified the treatment of classrel/arity clauses
|
changeset |
files
|
| 2007-04-12 |
haftmann |
canonical merge operations
|
changeset |
files
|