2006-11-22 haftmann 2006-11-22 no explicit check for theory Nat
2006-11-22 haftmann 2006-11-22 added code lemmas
2006-11-22 haftmann 2006-11-22 does not import Hilber_Choice any longer
2006-11-22 haftmann 2006-11-22 cleanup
2006-11-22 haftmann 2006-11-22 incorporated structure HOList into HOLogic
2006-11-22 haftmann 2006-11-22 dropped eq const
2006-11-22 haftmann 2006-11-22 removed Extraction dependency
2006-11-22 haftmann 2006-11-22 final draft
2006-11-21 wenzelm 2006-11-21 made SML/NJ happy;
2006-11-21 wenzelm 2006-11-21 theorem(_i): note assms of statement;
2006-11-21 wenzelm 2006-11-21 removed obsolete simple_note_thms;
2006-11-21 wenzelm 2006-11-21 added assmsN;
2006-11-21 wenzelm 2006-11-21 * Isar: the assumptions of a long theorem statement are available as assms;
2006-11-21 wenzelm 2006-11-21 activated x86_64-linux;
2006-11-21 wenzelm 2006-11-21 renamed Proof.put_thms_internal to Proof.put_thms;
2006-11-21 wenzelm 2006-11-21 simplified Proof.theorem(_i); moved theorem kinds from PureThy to Thm;
2006-11-21 wenzelm 2006-11-21 added stmt mode, which affects naming/indexing of local facts; renamed put_thms_internal to put_thms; notes: proper name and kind (outside of proof body); removed dead code;
2006-11-21 wenzelm 2006-11-21 simplified theorem(_i); notes: proper kind; renamed put_thms_internal to put_thms;
2006-11-21 wenzelm 2006-11-21 notes: proper kind; simplified Proof.theorem(_i); context_statement: ProofContext.set_stmt after import;
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_;