2000-07-23 wenzelm 2000-07-23 classical atts now intro! / intro / intro?;
2000-07-23 wenzelm 2000-07-23 renamed "Directories" to "Sessions";
2000-07-23 wenzelm 2000-07-23 tuned;
2000-07-22 wenzelm 2000-07-22 improved error msg; thm foo.cases;
2000-07-21 nipkow 2000-07-21 added ex_someI
2000-07-21 paulson 2000-07-21 much tidying in connection with the 2nd UNITY paper
2000-07-21 oheimb 2000-07-21 strengthened force_tac by using new first_best_tac
2000-07-21 oheimb 2000-07-21 removed safe_asm_full_simp_tac
2000-07-21 oheimb 2000-07-21 added map_upd_nonempty, also to simpset
2000-07-21 oheimb 2000-07-21 removed weaker variant of subset_insert_iff
2000-07-21 oheimb 2000-07-21 removed safe_asm_full_simp_tac, added generic_simp_tac
2000-07-21 prensani 2000-07-21 Updating of some comments
2000-07-21 nipkow 2000-07-21 *** empty log message ***
2000-07-21 paulson 2000-07-21 Univ no longer requires Arith (really it never did)
2000-07-20 wenzelm 2000-07-20 tuned;
2000-07-19 oheimb 2000-07-19 corrected header
2000-07-19 paulson 2000-07-19 changed / to // for quotienting
2000-07-19 paulson 2000-07-19 changed / to // for quotienting; general tidying
2000-07-19 paulson 2000-07-19 renamed // to / (which is what we want anyway) to avoid clash with the new use of // for quotienting
2000-07-19 paulson 2000-07-19 deleted redundant proof
2000-07-19 paulson 2000-07-19 // change; also moved entry for AddIffs
2000-07-18 wenzelm 2000-07-18 addsplits [split_if];
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;