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.
2006-07-11 ballarin 2006-07-11 New function transfer_witness lifting Thm.transfer to witnesses.
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski)
2006-07-10 webertj 2006-07-10 minor optimization wrt. certifying terms
2006-07-08 wenzelm 2006-07-08 tuned;
2006-07-08 wenzelm 2006-07-08 tuned;
2006-07-08 wenzelm 2006-07-08 updated;
2006-07-08 wenzelm 2006-07-08 tuned interface; case_ss: proper context;
2006-07-08 wenzelm 2006-07-08 tuned interface;
2006-07-08 wenzelm 2006-07-08 removed dead code;
2006-07-08 wenzelm 2006-07-08 Element.prove_witness: context; Goal.prove_global;
2006-07-08 wenzelm 2006-07-08 prove_witness: context;
2006-07-08 wenzelm 2006-07-08 tuned exception handling;
2006-07-08 wenzelm 2006-07-08 prove/prove_multi: context; prove_global: theory + standard; tuned;
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead; misc cleanup;
2006-07-08 wenzelm 2006-07-08 distinct simproc/simpset: proper context;
2006-07-08 wenzelm 2006-07-08 presburger_ss: proper context;
2006-07-08 wenzelm 2006-07-08 presburger_ss: proper context; Goal.prove: context;
2006-07-08 wenzelm 2006-07-08 tuned;
2006-07-08 wenzelm 2006-07-08 avoid Force_tac, which uses a different context;
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;