2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-09 krauss 2009-07-09 move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
2009-07-09 krauss 2009-07-09 drop unused lemmas
2009-07-09 chaieb 2009-07-09 FPS form a metric space, which justifies the infinte sum notation
2009-07-09 chaieb 2009-07-09 merged
2009-07-05 chaieb 2009-07-05 merged
2009-07-04 chaieb 2009-07-04 merged
2009-07-04 chaieb 2009-07-04 merged
2009-07-02 chaieb 2009-07-02 Gettring rid of sorts hyps
2009-07-08 haftmann 2009-07-08 tuned structure Code internally
2009-07-08 nipkow 2009-07-08 merged
2009-07-08 nipkow 2009-07-08 name fixed
2009-07-07 haftmann 2009-07-07 merged
2009-07-07 haftmann 2009-07-07 merged
2009-07-07 haftmann 2009-07-07 tuned interface of structure Code
2009-07-07 haftmann 2009-07-07 more accurate certificates for constant aliasses
2009-07-07 haftmann 2009-07-07 merged
2009-07-07 haftmann 2009-07-07 Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
2009-07-07 wenzelm 2009-07-07 fixed proof (cf. 40501bb2d57c);
2009-07-07 nipkow 2009-07-07 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-07-07 haftmann 2009-07-07 merged
2009-07-06 haftmann 2009-07-06 tuned code
2009-07-06 haftmann 2009-07-06 moved Inductive.myinv to Fun.inv; tuned
2009-07-07 wenzelm 2009-07-07 add_classrel/arity: strip_shyps of stored result;
2009-07-06 wenzelm 2009-07-06 clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;
2009-07-06 wenzelm 2009-07-06 witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-07-06 wenzelm 2009-07-06 clarified Thm.of_class/of_sort/class_triv;
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-04 wenzelm 2009-07-04 renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);
2009-07-04 wenzelm 2009-07-04 Delayed action.
2009-07-04 wenzelm 2009-07-04 merged
2009-07-04 haftmann 2009-07-04 merged
2009-07-03 haftmann 2009-07-03 nominal.ML is nominal_datatype.ML
2009-07-03 haftmann 2009-07-03 merged
2009-07-03 haftmann 2009-07-03 nominal.ML is nominal_datatype.ML
2009-07-03 haftmann 2009-07-03 cleaned up fundamental iml term functions; nested patterns
2009-07-03 haftmann 2009-07-03 cleaned up fundamental iml term functions
2009-07-03 haftmann 2009-07-03 proper closures -- imperative programming considered harmful...
2009-07-03 haftmann 2009-07-03 avoid useless code equations
2009-07-03 haftmann 2009-07-03 restored subscripts
2009-07-03 haftmann 2009-07-03 lemma foldl_apply_inv
2009-07-04 wenzelm 2009-07-04 is_open: surrogate sequence is High..Low; added class Index for decoding offsets; tuned;
2009-07-03 wenzelm 2009-07-03 init/check Isabelle_System;
2009-07-03 wenzelm 2009-07-03 init isabelle home from existing setting or hint via system property;
2009-07-03 wenzelm 2009-07-03 more hgignore;
2009-07-03 wenzelm 2009-07-03 basic setup for Isabelle/JVM application bundle;
2009-07-03 wenzelm 2009-07-03 separate setup for App1;
2009-07-03 wenzelm 2009-07-03 SCALA_HOME: proper line escapes for choosefrom;
2009-07-03 wenzelm 2009-07-03 allow reloading of settings within JVM process;
2009-07-03 wenzelm 2009-07-03 Isabelle application wrapper for windows.
2009-07-03 wenzelm 2009-07-03 isabelle.home: native jvmpath;
2009-07-03 wenzelm 2009-07-03 Generic Isabelle application wrapper.
2009-07-03 wenzelm 2009-07-03 observe SCALA_HOME, if available; no default classpath for scala-library.jar;
2009-07-02 wenzelm 2009-07-02 merged
2009-07-02 wenzelm 2009-07-02 recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
2009-07-02 haftmann 2009-07-02 merged
2009-07-02 haftmann 2009-07-02 instance arities can be simultaneous
2009-07-02 haftmann 2009-07-02 updated generated files
2009-07-02 haftmann 2009-07-02 more friendly wrt. PGs interpretation of compound *); added dedicated section on value and quickcheck