2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-12-07 haftmann 2007-12-07 proper treatment of code theorems for primrec
2007-12-07 haftmann 2007-12-07 dropped Instance.instantiate
2007-12-07 krauss 2007-12-07 Adding "ex/Induction_Scheme.thy" to tests
2007-12-07 krauss 2007-12-07 experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
2007-12-07 haftmann 2007-12-07 tuned further
2007-12-06 wenzelm 2007-12-06 renamed ML_PID to PID;
2007-12-06 nipkow 2007-12-06 R&F: added sgn lemma Prefix: sledge-hammered
2007-12-06 haftmann 2007-12-06 temporary code generator work arounds
2007-12-06 haftmann 2007-12-06 fixed slip
2007-12-06 haftmann 2007-12-06 -authentic primrec
2007-12-06 haftmann 2007-12-06 dropped legacy bindings
2007-12-06 haftmann 2007-12-06 authentic primrec
2007-12-06 haftmann 2007-12-06 dropped void space
2007-12-06 haftmann 2007-12-06 added new primrec package
2007-12-06 krauss 2007-12-06 load sum_tree.ML
2007-12-06 krauss 2007-12-06 factored out handling of sum types again
2007-12-06 wenzelm 2007-12-06 added test_markup; added channel markup and specials;
2007-12-06 wenzelm 2007-12-06 moved basic test_markup to isabelle_process.ML;
2007-12-06 wenzelm 2007-12-06 added channels; added markup operation, which operates on plain strings instead of raw output;
2007-12-06 wenzelm 2007-12-06 replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
2007-12-06 wenzelm 2007-12-06 check persistent sessions;
2007-12-05 wenzelm 2007-12-05 tuned signature;
2007-12-05 wenzelm 2007-12-05 made SML/NJ happy;
2007-12-05 wenzelm 2007-12-05 removed -e flag from most sessions;
2007-12-05 obua 2007-12-05 instance int,real :: lordered_ring
2007-12-05 krauss 2007-12-05 methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
2007-12-05 haftmann 2007-12-05 tuned class parts
2007-12-05 haftmann 2007-12-05 dropped Classpackage.thy
2007-12-05 haftmann 2007-12-05 tuned
2007-12-05 haftmann 2007-12-05 added parser for multi_arity
2007-12-05 haftmann 2007-12-05 added constrain_thm
2007-12-05 haftmann 2007-12-05 canonical instantiation
2007-12-05 haftmann 2007-12-05 map_product and fold_product
2007-12-05 haftmann 2007-12-05 interface and distinct simproc tuned
2007-12-05 haftmann 2007-12-05 improved
2007-12-05 haftmann 2007-12-05 interpretation of typedefs
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-12-05 haftmann 2007-12-05 added something about instantiation target
2007-12-05 kleing 2007-12-05 switch poly to 5.1, removed -e flag from most sessions
2007-12-05 kleing 2007-12-05 switch at-poly main to poly 5.1
2007-12-05 kleing 2007-12-05 make mac-poly non-experimental
2007-12-05 kleing 2007-12-05 make at64 non-experimental
2007-12-04 wenzelm 2007-12-04 Isabelle process wrapper -- interaction via external program.
2007-12-04 wenzelm 2007-12-04 Toplevel.loop: explicit argument for secure loop, no warning on quit;
2007-12-04 wenzelm 2007-12-04 added Isar.secure_main; pass Secure.is_secure to Toplevel.loop;
2007-12-04 wenzelm 2007-12-04 added Tools/isabelle_process.ML;
2007-12-04 wenzelm 2007-12-04 isabelle process: replaced option -p by -W (process wrapper);
2007-12-04 wenzelm 2007-12-04 replaced option -p by -W (process wrapper); tuned PGIP option setup;
2007-12-04 wenzelm 2007-12-04 \<chi> is now considered a letter; tuned;
2007-12-04 wenzelm 2007-12-04 symbol chi is also a letter;
2007-12-03 obua 2007-12-03 improvements
2007-12-03 haftmann 2007-12-03 overloading target
2007-12-03 haftmann 2007-12-03 interface for unchecked definitions
2007-12-03 haftmann 2007-12-03 shifted "fun" command to Wellfounded_Relations
2007-12-03 haftmann 2007-12-03 updated
2007-12-02 chaieb 2007-12-02 Eliminated unused theorems minusinf_ex and minusinf_bex
2007-11-30 haftmann 2007-11-30 first working version of instance target
2007-11-30 haftmann 2007-11-30 interpretation for typedefs
2007-11-30 haftmann 2007-11-30 using intro_locales instead of unfold_locales if appropriate