2000-07-18 wenzelm 2000-07-18 theorems foo.splits = foo.split foo.split_asm;
2000-07-18 wenzelm 2000-07-18 removed obsolete expand_if = split_if;
2000-07-18 wenzelm 2000-07-18 * HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm;
2000-07-18 wenzelm 2000-07-18 * HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm; datatype package provides theorems foo.splits = foo.split foo.split_asm for each datatype;
2000-07-18 wenzelm 2000-07-18 replaced arities by instance;
2000-07-18 kleing 2000-07-18 MicroJava structure changed
2000-07-17 wenzelm 2000-07-17 consts: include *all* names;
2000-07-17 bauerg 2000-07-17 tuded presentation;
2000-07-17 wenzelm 2000-07-17 AddXIs [UnI1, UnI2];
2000-07-17 kleing 2000-07-17 flat instruction set, op. semantics now in JVMExecInstr.thy
2000-07-17 kleing 2000-07-17 flat instruction set
2000-07-17 bauerg 2000-07-17 10pt
2000-07-17 bauerg 2000-07-17 - xsymbols for \<noteq> \<notin> \<in> \<exists> \<forall> \<and> \<inter> \<union> \<Union> - vector space type of {plus, minus, zero}, overload 0 in vector space - syntax |.| and ||.||
2000-07-16 wenzelm 2000-07-16 strip_prod_type = HOLogic.prodT_factors;
2000-07-16 wenzelm 2000-07-16 AST translation rules no longer require constant head on LHS;
2000-07-16 wenzelm 2000-07-16 fixed nested prod syntax;
2000-07-16 wenzelm 2000-07-16 use split_tupled_all;
2000-07-16 wenzelm 2000-07-16 use pair_tac; use split syntax;
2000-07-16 wenzelm 2000-07-16 adapted tuple syntax;
2000-07-16 wenzelm 2000-07-16 tuned;
2000-07-16 wenzelm 2000-07-16 use pair_tac;
2000-07-16 wenzelm 2000-07-16 use split syntax;
2000-07-16 wenzelm 2000-07-16 fixed tuple translations;
2000-07-16 wenzelm 2000-07-16 defs (overloaded);
2000-07-16 wenzelm 2000-07-16 added is_unitT; added proper versions of mk_tuple(T), dest_tuple(T) -- unused;
2000-07-16 wenzelm 2000-07-16 instance unit :: finite;
2000-07-16 wenzelm 2000-07-16 more robust tuple syntax (still improper, though!);
2000-07-16 wenzelm 2000-07-16 improved unit theory: unit_all_eq1, unit_all_eq2, split_all_tac; tuned;
2000-07-16 wenzelm 2000-07-16 added syntax for proper / improper selector functions;
2000-07-16 wenzelm 2000-07-16 tuned;
2000-07-16 wenzelm 2000-07-16 tuned;
2000-07-16 wenzelm 2000-07-16 avoid 'split';
2000-07-16 wenzelm 2000-07-16 added Tuple.thy;
2000-07-16 wenzelm 2000-07-16 added ex/Tuple.thy;
2000-07-16 wenzelm 2000-07-16 syntax (symbols) "op o" moved from HOL to Fun;
2000-07-16 wenzelm 2000-07-16 added finite_unit;
2000-07-16 wenzelm 2000-07-16 AST translation rules no longer require constant head on LHS;
2000-07-16 wenzelm 2000-07-16 * tuned AST representation of nested pairs, avoiding bogus output in case of overlap with user translations (e.g. judgements over tuples); * AST translation rules no longer require constant head on LHS;
2000-07-14 oheimb 2000-07-14 corrections (cast relation, Prog.ML -> Decl.ML)
2000-07-14 wenzelm 2000-07-14 improved add_edges_cyclic;
2000-07-14 oheimb 2000-07-14 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
2000-07-14 oheimb 2000-07-14 added (surjective_pairing RS sym) to simpset
2000-07-14 oheimb 2000-07-14 strengthened rtranclD
2000-07-14 oheimb 2000-07-14 added option_map_o_sum_case (also to simpset)
2000-07-14 oheimb 2000-07-14 added sum_case_empty_empty (also to simpset)
2000-07-14 oheimb 2000-07-14 tuned syntax
2000-07-14 oheimb 2000-07-14 added hint on fun_sum
2000-07-14 oheimb 2000-07-14 added fun_upd2_simproc
2000-07-14 oheimb 2000-07-14 re-added subset_empty to simpset
2000-07-14 paulson 2000-07-14 used bounded quantification in definition of guarantees and other minor adjustments
2000-07-14 paulson 2000-07-14 moved sublist from UNITY/AllocBase to List
2000-07-14 paulson 2000-07-14 AddIffs
2000-07-14 paulson 2000-07-14 parent should be Main
2000-07-14 paulson 2000-07-14 changed the quotient syntax from / to //
2000-07-13 wenzelm 2000-07-13 tuned cycle_msg;
2000-07-13 wenzelm 2000-07-13 updated;
2000-07-13 wenzelm 2000-07-13 HOL: the disjoint sum is now "<+>" instead of "Plus"; ML: PureThy.add_defs gets additional argument;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-07-13 wenzelm 2000-07-13 defs (overloaded);
2000-07-13 wenzelm 2000-07-13 tuned;