2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-08 wenzelm 2009-03-08 proper local context for text with antiquotations;
2009-03-08 wenzelm 2009-03-08 more explicit warning message;
2009-03-08 wenzelm 2009-03-08 added qualified_name -- emulates old-style qualified bstring; tuned;
2009-03-08 wenzelm 2009-03-08 added General/long_name.ML;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name; tuned signature;
2009-03-08 wenzelm 2009-03-08 index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
2009-03-08 wenzelm 2009-03-08 proper context for Simplifier.pretty_ss;
2009-03-08 wenzelm 2009-03-08 added dest_ss; proper context fo pretty_ss; tuned;
2009-03-08 wenzelm 2009-03-08 use binding type;
2009-03-08 wenzelm 2009-03-08 merged
2009-03-07 haftmann 2009-03-07 merged
2009-03-07 haftmann 2009-03-07 restructured theory Set.thy
2009-03-07 wenzelm 2009-03-07 merged
2009-03-07 blanchet 2009-03-07 Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
2009-03-07 blanchet 2009-03-07 Added a second timeout mechanism to Refute. For some reason, TimeLimit.timeLimit often does not work, and it leaves Refute running forever, making any evaluation using Mutabelle or Mirabelle impossible. The redundant timeout seems to do the trick.
2009-03-07 blanchet 2009-03-07 merged
2009-03-07 blanchet 2009-03-07 Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
2009-03-07 wenzelm 2009-03-07 minimal adaptions for abstract binding type;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in packages;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-07 wenzelm 2009-03-07 replace old bstring by binding for logical primitives: class, type, const etc.;
2009-03-07 wenzelm 2009-03-07 moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;
2009-03-07 wenzelm 2009-03-07 adapted Syntax.const_name;
2009-03-07 wenzelm 2009-03-07 canonical argument order for type_name, const_name;
2009-03-07 wenzelm 2009-03-07 added const_binding;
2009-03-07 wenzelm 2009-03-07 added prefix_name, suffix_name; added eq_name; added opaque signature constraint to prevent accidental equality test;
2009-03-07 wenzelm 2009-03-07 Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-07 wenzelm 2009-03-07 renamed rep_ss to MetaSimplifier.internal_ss;
2009-03-07 wenzelm 2009-03-07 Binding.str_of: removed verbose feature, include qualifier in output; renamed Binding.add_prefix to Binding.prefix;
2009-03-07 wenzelm 2009-03-07 oracle: proper name position, tuned;
2009-03-07 haftmann 2009-03-07 merged
2009-03-07 haftmann 2009-03-07 drop poisonous code equations
2009-03-07 haftmann 2009-03-07 suppress document output
2009-03-06 haftmann 2009-03-06 theory with syntax for lattice operations
2009-03-06 haftmann 2009-03-06 added babel -- necessary for bind infix syntax
2009-03-06 haftmann 2009-03-06 added enumeration of predicates
2009-03-06 haftmann 2009-03-06 moved instance option :: finite to Option.thy
2009-03-06 haftmann 2009-03-06 constructive version of Cantor's first diagonalization argument
2009-03-06 haftmann 2009-03-06 equalities for Min, Max
2009-03-06 wenzelm 2009-03-06 merged
2009-03-06 nipkow 2009-03-06 added lemma
2009-03-06 nipkow 2009-03-06 merged
2009-03-06 nipkow 2009-03-06 Docs
2009-03-06 wenzelm 2009-03-06 eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-06 wenzelm 2009-03-06 schedule_seq: handle after_load errors as in schedule_futures;
2009-03-06 wenzelm 2009-03-06 replaced archaic use of rep_ss by Simplifier.mksimps;
2009-03-06 wenzelm 2009-03-06 improved error handling for document antiquotations;
2009-03-06 blanchet 2009-03-06 merged
2009-03-06 nipkow 2009-03-06 merged
2009-03-06 blanchet 2009-03-06 Added "expect" option to Refute, like in Nitpick, that allows to write regression tests. Also replaced calls to "Output.immediate_output" with "priority" or "tracing", because "immediate_output" causes some problems (as explained by Makarius to Sascha).
2009-03-06 nipkow 2009-03-06 added lemmas
2009-03-06 blanchet 2009-03-06 Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead. I tested the affected symbols (card, finite, lfp, and gfp), and Refute now works better than before (i.e., more precision and more speed).
2009-03-06 blanchet 2009-03-06 merged
2009-03-06 blanchet 2009-03-06 merged
2009-03-06 blanchet 2009-03-06 Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
2009-03-06 haftmann 2009-03-06 merged
2009-03-06 haftmann 2009-03-06 merged
2009-03-06 haftmann 2009-03-06 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05 haftmann 2009-03-05 merged