2006-07-14 wenzelm 2006-07-14 keep/transaction: unified execution model (with debugging etc.); tuned;
2006-07-14 webertj 2006-07-14 trivial whitespace changes
2006-07-14 wenzelm 2006-07-14 simp method: depth_limit;
2006-07-13 paulson 2006-07-13 "conjecture" must be lower case
2006-07-13 wenzelm 2006-07-13 tuned insert_list;
2006-07-13 wenzelm 2006-07-13 Name.context already declares empty names; tune ins_sorts -- sort assigments should never change later;
2006-07-13 wenzelm 2006-07-13 strip_abs_eta: proper use of Name.context;
2006-07-13 wenzelm 2006-07-13 do not export make_context; initial context: declare empty names; variants: no special treatment of empty names;
2006-07-13 wenzelm 2006-07-13 removed colon from sym category;
2006-07-13 paulson 2006-07-13 fix to refl_clause_aux: added occurs check
2006-07-12 wenzelm 2006-07-12 * Isar: ":" (colon) is no longer a symbolic identifier character;
2006-07-12 wenzelm 2006-07-12 removed duplicate of Tactic.make_elim_preserve;
2006-07-12 wenzelm 2006-07-12 removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);
2006-07-12 wenzelm 2006-07-12 exported make_elim_preserve;
2006-07-12 wenzelm 2006-07-12 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars; tuned;
2006-07-12 wenzelm 2006-07-12 simplified prove_conv;
2006-07-12 wenzelm 2006-07-12 removed ':' from category of symbolic identifier chars;
2006-07-12 wenzelm 2006-07-12 query/bang_colon: separate tokens;
2006-07-12 haftmann 2006-07-12 purged website sources
2006-07-12 haftmann 2006-07-12 added strip_abs_eta
2006-07-12 haftmann 2006-07-12 added chop_prefix
2006-07-12 haftmann 2006-07-12 class_of_param instead of class_of
2006-07-12 haftmann 2006-07-12 adaptions in class_package
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-07-12 wenzelm 2006-07-12 variants: special treatment of empty name;
2006-07-11 wenzelm 2006-07-11 avoid reference to internal skolem;
2006-07-11 wenzelm 2006-07-11 separate names filed (covers fixes/defaults);
2006-07-11 wenzelm 2006-07-11 adapted Name.defaults_of;
2006-07-11 wenzelm 2006-07-11 removed obsolete xless; tuned zero_var_indexes;
2006-07-11 wenzelm 2006-07-11 clean: no special treatment of empty name; declare, invent: clean arguments;
2006-07-11 wenzelm 2006-07-11 removed obsolete xless;
2006-07-11 webertj 2006-07-11 replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
2006-07-11 wenzelm 2006-07-11 uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;
2006-07-11 wenzelm 2006-07-11 replaced read_radixint by read_intinf;
2006-07-11 wenzelm 2006-07-11 removed str_to_int in favour of general Syntax.read_xnum;
2006-07-11 wenzelm 2006-07-11 num/xnum: bin or hex;
2006-07-11 wenzelm 2006-07-11 Name.internal; Name.invent_list;
2006-07-11 wenzelm 2006-07-11 tuned;
2006-07-11 wenzelm 2006-07-11 * Pure: structure Name;
2006-07-11 wenzelm 2006-07-11 Names of basic logical entities (variables etc.).
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); removed obsolete mem_term;
2006-07-11 wenzelm 2006-07-11 Name.internal; Name.dest_skolem;
2006-07-11 wenzelm 2006-07-11 adapted to more efficient Name/Variable implementation; removed dead code;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.internal;
2006-07-11 wenzelm 2006-07-11 maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML);
2006-07-11 wenzelm 2006-07-11 removed obsolete mem_ix;
2006-07-11 wenzelm 2006-07-11 removed obsolete ins_ix, mem_ix, ins_term, mem_term; moved variant(list), invent_names, bound, dest_internal/skolem etc. to name.ML;
2006-07-11 wenzelm 2006-07-11 Name.dest_skolem;
2006-07-11 wenzelm 2006-07-11 Name.bound;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.bound;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.invent_list;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.clean;
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-07-11 wenzelm 2006-07-11 added name.ML;
2006-07-11 wenzelm 2006-07-11 Name.is_bound;
2006-07-11 wenzelm 2006-07-11 removed obsolete mem_term;
2006-07-11 wenzelm 2006-07-11 Name.internal;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-11 wenzelm 2006-07-11 let_simproc: activate Variable.import;
2006-07-11 ballarin 2006-07-11 Witness theorems of interpretations now transfered to current theory.