isabelle: Graph

adapted to simplified ThyOutput.antiquotation interface;
2009-03-09, by wenzelm
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
2009-03-09, by wenzelm
merged
2009-03-09, by wenzelm
merged
2009-03-09, by haftmann
NameSpace.base_name ~> Long_Name.base_name
2009-03-09, by haftmann
Docs
2009-03-09, by nipkow
merged
2009-03-09, by nipkow
fixed typing of UN/INT syntax
2009-03-09, by nipkow
more contributors;
2009-03-09, by wenzelm
adapted ThyOutput.antiquotation;
2009-03-09, by wenzelm
refined antiquotation interface: formally pass result context and (potential) result source;
2009-03-09, by wenzelm
merged
2009-03-09, by haftmann
binding replaces bstring
2009-03-09, by haftmann
dropped eq_pred
2009-03-09, by haftmann
merged
2009-03-08, by haftmann
refined enumeration implementation
2009-03-08, by haftmann
added top and bot syntax
2009-03-08, by haftmann
added predicate compiler, as formally checked prototype, not as user package
2009-03-08, by haftmann
attempt to bypass spurious infix syntax problem on polyml/sun
2009-03-09, by haftmann
UN syntax fix
2009-03-09, by nipkow
merged
2009-03-09, by nipkow
Docs updates
2009-03-09, by nipkow
use simplified ThyOutput.antiquotation;
2009-03-08, by wenzelm
added (raw_)antiquotation -- simplified wrapper for defining output commands;
2009-03-08, by wenzelm
simplified presentation: pass state directly;
2009-03-08, by wenzelm
simplified presentation: built into transaction, pass state directly;
2009-03-08, by wenzelm
adapted to structure Long_Name;
2009-03-08, by wenzelm
moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-08, by wenzelm
proper local context for text with antiquotations;
2009-03-08, by wenzelm
more explicit warning message;
2009-03-08, by wenzelm
added qualified_name -- emulates old-style qualified bstring;
2009-03-08, by wenzelm
added General/long_name.ML;
2009-03-08, by wenzelm
moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-08, by wenzelm
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
2009-03-08, by wenzelm
proper context for Simplifier.pretty_ss;
2009-03-08, by wenzelm
added dest_ss;
2009-03-08, by wenzelm
use binding type;
2009-03-08, by wenzelm
merged
2009-03-08, by wenzelm
merged
2009-03-07, by haftmann
restructured theory Set.thy
2009-03-07, by haftmann
merged
2009-03-07, by wenzelm
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
2009-03-07, by blanchet
Added a second timeout mechanism to Refute.
2009-03-07, by blanchet
merged
2009-03-07, by blanchet
Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
2009-03-07, by blanchet
minimal adaptions for abstract binding type;
2009-03-07, by wenzelm
more uniform handling of binding in packages;
2009-03-07, by wenzelm
more uniform handling of binding in targets and derived elements;
2009-03-07, by wenzelm
replace old bstring by binding for logical primitives: class, type, const etc.;
2009-03-07, by wenzelm
moved Thm.def_name(_optional) to more_thm.ML;
2009-03-07, by wenzelm
adapted Syntax.const_name;
2009-03-07, by wenzelm
canonical argument order for type_name, const_name;
2009-03-07, by wenzelm
added const_binding;
2009-03-07, by wenzelm
added prefix_name, suffix_name;
2009-03-07, by wenzelm
Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-07, by wenzelm
renamed rep_ss to MetaSimplifier.internal_ss;
2009-03-07, by wenzelm
Binding.str_of: removed verbose feature, include qualifier in output;
2009-03-07, by wenzelm
oracle: proper name position, tuned;
2009-03-07, by wenzelm
merged
2009-03-07, by haftmann
drop poisonous code equations
2009-03-07, by haftmann
suppress document output
2009-03-07, by haftmann
theory with syntax for lattice operations
2009-03-06, by haftmann
added babel -- necessary for bind infix syntax
2009-03-06, by haftmann
added enumeration of predicates
2009-03-06, by haftmann
moved instance option :: finite to Option.thy
2009-03-06, by haftmann
constructive version of Cantor's first diagonalization argument
2009-03-06, by haftmann
equalities for Min, Max
2009-03-06, by haftmann
merged
2009-03-06, by wenzelm
added lemma
2009-03-06, by nipkow
merged
2009-03-06, by nipkow
Docs
2009-03-06, by nipkow
eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-06, by wenzelm
schedule_seq: handle after_load errors as in schedule_futures;
2009-03-06, by wenzelm
replaced archaic use of rep_ss by Simplifier.mksimps;
2009-03-06, by wenzelm
improved error handling for document antiquotations;
2009-03-06, by wenzelm
merged
2009-03-06, by blanchet
merged
2009-03-06, by nipkow
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
2009-03-06, by blanchet
added lemmas
2009-03-06, by nipkow
Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead.
2009-03-06, by blanchet
merged
2009-03-06, by blanchet
merged
2009-03-06, by blanchet
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
2009-03-06, by blanchet
merged
2009-03-06, by haftmann
merged
2009-03-06, by haftmann
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-06, by haftmann
merged
2009-03-05, by haftmann
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05, by haftmann
tuned
2009-03-05, by haftmann
moved complete_lattice to Set.thy
2009-03-05, by haftmann
dropped Id
2009-03-05, by haftmann
corrected slip in NEWS
2009-03-06, by haftmann
merged
2009-03-06, by haftmann
added strict_mono predicate
2009-03-06, by haftmann
Identifiers of some old CVS file versions;
2009-03-06, by wenzelm
recovered generated files;
2009-03-06, by wenzelm
more precise deps;
2009-03-06, by wenzelm
merged
2009-03-06, by nipkow
Added Docs
2009-03-06, by nipkow
render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
2009-03-05, by wenzelm
removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
2009-03-05, by wenzelm
removed unused TableFun().fold_map and GraphFun().fold_map_nodes;
2009-03-05, by wenzelm
removed spurious occurrences of old rep_ss;
2009-03-05, by wenzelm
Thm.add_oracle interface: replaced old bstring by binding;
2009-03-05, by wenzelm
silent chmod;
2009-03-05, by wenzelm
Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05, by wenzelm
close_schematic_term: uniform order of types/terms;
2009-03-05, by wenzelm
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05, by wenzelm
TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
2009-03-05, by wenzelm
fixed proofs -- follow-up to ecd6f0ca62ea;
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name");
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name;
2009-03-05, by wenzelm
eliminated obsolete ProofContext.full_bname;
2009-03-05, by wenzelm
Binding.prefix_of;
2009-03-05, by wenzelm
adapted Binding.dest;
2009-03-05, by wenzelm
added prefix_of;
2009-03-05, by wenzelm
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-05, by blanchet
merged
2009-03-05, by wenzelm
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04, by huffman
regenerated document;
2009-03-05, by wenzelm
merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
2009-03-05, by wenzelm
dummy changes to produce a new changeset of these files;
2009-03-05, by wenzelm
updated generated file -- changed since @{ML} now ignores source flag;
2009-03-05, by wenzelm
fixed document;
2009-03-05, by wenzelm
removed old/broken CVS Ids;
2009-03-04, by wenzelm
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
2009-03-04, by wenzelm
merged
2009-03-04, by chaieb
Moved general theorems about sums and products to FiniteSet.thy
2009-03-04, by chaieb
fixed proofs; added rules as default simp-rules
2009-03-04, by chaieb
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
2009-03-04, by chaieb
Added Libray dependency on Topology_Euclidean_Space
2009-03-04, by chaieb
Added general theorems for fold_image, setsum and set_prod
2009-03-04, by chaieb
fixed proofs
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-02-25, by chaieb
merged
2009-02-25, by chaieb
Second try at adding "nitpick_const_def" attribute.
2009-03-04, by blanchet
Fix parentheses.
2009-03-04, by blanchet
merged
2009-03-04, by blanchet
Added "nitpick_const_simp" attribute to Nominal primrec.
2009-03-04, by blanchet
NEWS: renamed o2s to Option.set;
2009-03-04, by wenzelm
less arbitrary occurrences of undefined
2009-03-04, by haftmann
datatype antiquotation does not assume LaTeX as output any longer
2009-03-04, by haftmann
merged
2009-03-04, by nipkow
Option.thy
2009-03-04, by nipkow
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
2009-03-04, by haftmann
merged
2009-03-04, by haftmann
explicit error message for `improper` instances lacking explicit instance parameter constants
2009-03-04, by haftmann
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Made Refute.norm_rhs public, so I can use it in Nitpick.
2009-03-04, by blanchet
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
2009-03-01, by blanchet
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
2009-02-24, by blanchet
merged
2009-03-04, by nipkow
Made Option a separate theory and renamed option_map to Option.map
2009-03-04, by nipkow
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-04, by wenzelm
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
2009-03-03, by wenzelm
tuned str_of, now subject to verbose flag;
2009-03-03, by wenzelm
added @{binding} ML antiquotations;
2009-03-03, by wenzelm
added print_properties, print_position (again);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
merged
2009-03-03, by haftmann
tuned manuals
2009-03-03, by haftmann
more canonical directory structure of manuals
2009-03-03, by haftmann
merged
2009-03-03, by wenzelm
removed and renamed redundant lemmas
2009-03-03, by nipkow
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03, by wenzelm
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
2009-03-03, by wenzelm
added markup for binding;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
renamed Binding.display to Binding.str_of, which is slightly more canonical;
2009-03-03, by wenzelm
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
2009-03-03, by wenzelm
moved name space externalization flags back to name_space.ML;
2009-03-03, by wenzelm
moved name space externalization flags back to name_space.ML;
2009-03-03, by wenzelm
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
Thm.binding;
2009-03-03, by wenzelm
added type binding and val empty_binding;
2009-03-03, by wenzelm
updated generated files;
2009-03-03, by wenzelm
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
2009-03-03, by wenzelm
Implement Makarius's suggestion for improved type pattern parsing.
2009-03-03, by Timothy Bourke
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
2009-03-02, by Timothy Bourke
adapted to lates experimental version;
2009-03-02, by wenzelm
removed Ids;
2009-03-02, by wenzelm
merged
2009-03-02, by haftmann
reduced confusion code_funcgr vs. code_wellsorted
2009-03-02, by haftmann
better markup
2009-03-02, by haftmann
name fix
2009-03-02, by nipkow
merged
2009-03-02, by nipkow
name changes
2009-03-02, by nipkow
Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-03-02, by chaieb
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
2009-03-02, by chaieb
fixed broken @{file} refs;
2009-03-02, by wenzelm
merged
2009-03-02, by wenzelm
using plain ISABELLE_PROCESS
2009-03-02, by haftmann
merged
2009-03-02, by haftmann
ignore ISABELLE_LINE_EDITOR for code generation
2009-03-02, by haftmann
use long names for old-style fold combinators;
2009-03-01, by wenzelm
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-03-01, by wenzelm
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
2009-03-01, by wenzelm
end_timing: generalized result -- message plus with explicit time values;
2009-03-01, by wenzelm
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
2009-03-01, by wenzelm
updated contributors;
2009-03-01, by wenzelm
removed parts of the manual that are clearly obsolete, or covered by
2009-03-01, by wenzelm
merged
2009-03-01, by wenzelm
minor update of Mercurial HOWTO;
2009-03-01, by wenzelm
removed redundant lemmas
2009-03-01, by nipkow
added lemmas by Jeremy Avigad
2009-03-01, by nipkow
A Serbian theory, by Filip Maric.
2009-02-28, by wenzelm
more accurate deps;
2009-02-28, by wenzelm
merged
2009-02-28, by wenzelm
add news for HOLCF; fixed some typos and inaccuracies
2009-02-28, by huffman
fixed headers;
2009-02-28, by wenzelm
moved isabelle_system.scala to src/Pure/System/;
2009-02-28, by wenzelm
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2009-02-28, by wenzelm
updated generated files;
2009-02-28, by wenzelm
added method "coherent";
2009-02-28, by wenzelm
more refs;
2009-02-28, by wenzelm
moved method "iprover" to HOL specific part;
2009-02-28, by wenzelm
removed Ids;
2009-02-28, by wenzelm
simultaneous use_thys;
2009-02-28, by wenzelm
replaced low-level 'no_syntax' by 'no_notation';
2009-02-28, by wenzelm
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28, by wenzelm
tuned message;
2009-02-28, by wenzelm
* New prover for coherent logic (see src/Tools/coherent.ML).
2009-02-28, by wenzelm
more CONTRIBUTORS;
2009-02-28, by wenzelm
removed Ids;
2009-02-28, by wenzelm
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-28, by wenzelm
some updates on ancient README;
2009-02-28, by wenzelm
fixrec package uses new-style syntax and local-theory interface
2009-02-27, by huffman
add function taken_names
2009-02-27, by huffman
merged
2009-02-27, by huffman
make list-style polynomial syntax work when show_sorts is on
2009-02-27, by huffman
more CONTRIBUTORS;
2009-02-27, by wenzelm
turned "read-only refs" typ_level and minimize_applies into constant values;
2009-02-27, by wenzelm
merged
2009-02-27, by wenzelm