2006-11-21 wenzelm 2006-11-21 notes: proper kind;
2006-11-21 wenzelm 2006-11-21 removed kind attribs;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm; exported note_thms(s);
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm;
2006-11-21 wenzelm 2006-11-21 LocalTheory.notes/defs: proper kind;
2006-11-21 wenzelm 2006-11-21 LocalTheory.axioms/notes/defs: proper kind; simplified Proof.theorem(_i);
2006-11-21 wenzelm 2006-11-21 simplified Proof.theorem(_i);
2006-11-21 wenzelm 2006-11-21 LocalTheory.axioms/notes/defs: proper kind; context_notes: ProofContext.set_stmt after import;
2006-11-21 paulson 2006-11-21 Optimized class_pairs for the common case of no subclasses
2006-11-21 paulson 2006-11-21 Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
2006-11-21 paulson 2006-11-21 New transformation of eliminatino rules: we simply replace the final conclusion variable by False
2006-11-21 kleing 2006-11-21 run poly-4.9.1 as stable and poly-4.2.0 as experimental on at
2006-11-21 wenzelm 2006-11-21 removed legacy ML setup;
2006-11-21 wenzelm 2006-11-21 converted legacy ML scripts;
2006-11-20 wenzelm 2006-11-20 converted legacy ML scripts;
2006-11-20 wenzelm 2006-11-20 HOL-Prolog: converted legacy ML scripts;
2006-11-20 kleing 2006-11-20 start at-sml earlier and on different machine, remove sun-sml test (takes too long)
2006-11-19 wenzelm 2006-11-19 HOL-Algebra: converted legacy ML scripts;
2006-11-19 webertj 2006-11-19 profiling disabled
2006-11-18 haftmann 2006-11-18 code thms for classops violating type discipline ignored
2006-11-18 haftmann 2006-11-18 cleanup
2006-11-18 haftmann 2006-11-18 added instance for class size
2006-11-18 haftmann 2006-11-18 added combinators and lemmas
2006-11-18 haftmann 2006-11-18 using class instance
2006-11-18 haftmann 2006-11-18 dvd_def now with object equality
2006-11-18 haftmann 2006-11-18 op div/op mod now named without leading op
2006-11-18 haftmann 2006-11-18 workaround for definition violating type discipline
2006-11-18 haftmann 2006-11-18 moved dvd stuff to theory Divides
2006-11-18 haftmann 2006-11-18 re-eliminated thm trichotomy
2006-11-18 haftmann 2006-11-18 power is now a class
2006-11-18 haftmann 2006-11-18 tuned
2006-11-18 haftmann 2006-11-18 clarified module dependencies
2006-11-18 haftmann 2006-11-18 div is now a class
2006-11-18 haftmann 2006-11-18 reduced verbosity
2006-11-18 haftmann 2006-11-18 adjustments for class package
2006-11-17 urbanc 2006-11-17 added an intro lemma for freshness of products; set up the simplifier so that it can deal with the compact and long notation for freshness constraints (FIXME: it should also be able to deal with the special case of freshness of atoms)
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-17 wenzelm 2006-11-17 'notation': more robust 'and' list;
2006-11-17 wenzelm 2006-11-17 updated;
2006-11-17 wenzelm 2006-11-17 added Isar.goal;
2006-11-17 wenzelm 2006-11-17 added where_;
2006-11-16 huffman 2006-11-16 add lemmas LIM_zero_iff, LIM_norm_zero_iff
2006-11-16 paulson 2006-11-16 Includes type:sort constraints in its code to collect predicates in axiom clauses.
2006-11-16 paulson 2006-11-16 Now includes only types used to instantiate overloaded constants in arity clauses
2006-11-16 wenzelm 2006-11-16 added General/basics.ML;
2006-11-16 wenzelm 2006-11-16 moved some fundamental concepts to General/basics.ML;
2006-11-16 wenzelm 2006-11-16 Fundamental concepts.
2006-11-15 wenzelm 2006-11-15 add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
2006-11-15 wenzelm 2006-11-15 tuned proofs;
2006-11-15 wenzelm 2006-11-15 replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
2006-11-15 wenzelm 2006-11-15 replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; declared intro/elim rules;
2006-11-15 haftmann 2006-11-15 dropping accidental self-imports
2006-11-15 haftmann 2006-11-15 corrected polymorphism check
2006-11-15 haftmann 2006-11-15 clarified code for building function equation system; explicit check of type discipline
2006-11-15 haftmann 2006-11-15 moved evaluation to Code_Generator.thy
2006-11-15 haftmann 2006-11-15 added filter_set; adaptions to more strict type discipline for code lemmas
2006-11-15 haftmann 2006-11-15 moved transitivity rules to Orderings.thy
2006-11-15 haftmann 2006-11-15 added transitivity rules, reworking of min/max lemmas
2006-11-15 haftmann 2006-11-15 dropped dependency on sets
2006-11-15 haftmann 2006-11-15 reworking of min/max lemmas