isabelle: Graph

consts: ProofContext.set_stmt true -- avoids naming of local thms;
2006-11-22, by wenzelm
init: enter inner statement mode, which prevents local notes from being named internally;
2006-11-22, by wenzelm
more careful declaration of "intros" as Pure.intro;
2006-11-22, by wenzelm
Fix to local file URI syntax. Add first part of lexicalstructure command support.
2006-11-22, by aspinall
completed class parameter handling in axclass.ML
2006-11-22, by haftmann
added Isar syntax for adding parameters to axclasses
2006-11-22, by haftmann
forced name prefix for class operations
2006-11-22, by haftmann
example tuned
2006-11-22, by haftmann
no explicit check for theory Nat
2006-11-22, by haftmann
added code lemmas
2006-11-22, by haftmann
does not import Hilber_Choice any longer
2006-11-22, by haftmann
cleanup
2006-11-22, by haftmann
incorporated structure HOList into HOLogic
2006-11-22, by haftmann
dropped eq const
2006-11-22, by haftmann
removed Extraction dependency
2006-11-22, by haftmann
final draft
2006-11-22, by haftmann
made SML/NJ happy;
2006-11-21, by wenzelm
theorem(_i): note assms of statement;
2006-11-21, by wenzelm
removed obsolete simple_note_thms;
2006-11-21, by wenzelm
added assmsN;
2006-11-21, by wenzelm
* Isar: the assumptions of a long theorem statement are available as assms;
2006-11-21, by wenzelm
activated x86_64-linux;
2006-11-21, by wenzelm
renamed Proof.put_thms_internal to Proof.put_thms;
2006-11-21, by wenzelm
simplified Proof.theorem(_i);
2006-11-21, by wenzelm
added stmt mode, which affects naming/indexing of local facts;
2006-11-21, by wenzelm
simplified theorem(_i);
2006-11-21, by wenzelm
notes: proper kind;
2006-11-21, by wenzelm
notes: proper kind;
2006-11-21, by wenzelm
removed kind attribs;
2006-11-21, by wenzelm
moved theorem kinds from PureThy to Thm;
2006-11-21, by wenzelm
moved theorem kinds from PureThy to Thm;
2006-11-21, by wenzelm
LocalTheory.notes/defs: proper kind;
2006-11-21, by wenzelm
LocalTheory.axioms/notes/defs: proper kind;
2006-11-21, by wenzelm
simplified Proof.theorem(_i);
2006-11-21, by wenzelm
LocalTheory.axioms/notes/defs: proper kind;
2006-11-21, by wenzelm
Optimized class_pairs for the common case of no subclasses
2006-11-21, by paulson
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
2006-11-21, by paulson
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
2006-11-21, by paulson
run poly-4.9.1 as stable and poly-4.2.0 as experimental on at
2006-11-21, by kleing
removed legacy ML setup;
2006-11-21, by wenzelm
converted legacy ML scripts;
2006-11-21, by wenzelm
converted legacy ML scripts;
2006-11-20, by wenzelm
HOL-Prolog: converted legacy ML scripts;
2006-11-20, by wenzelm
start at-sml earlier and on different machine, remove sun-sml test (takes too long)
2006-11-20, by kleing
HOL-Algebra: converted legacy ML scripts;
2006-11-19, by wenzelm
profiling disabled
2006-11-19, by webertj
code thms for classops violating type discipline ignored
2006-11-18, by haftmann
cleanup
2006-11-18, by haftmann
added instance for class size
2006-11-18, by haftmann
added combinators and lemmas
2006-11-18, by haftmann
using class instance
2006-11-18, by haftmann
dvd_def now with object equality
2006-11-18, by haftmann
op div/op mod now named without leading op
2006-11-18, by haftmann
workaround for definition violating type discipline
2006-11-18, by haftmann
moved dvd stuff to theory Divides
2006-11-18, by haftmann
re-eliminated thm trichotomy
2006-11-18, by haftmann
power is now a class
2006-11-18, by haftmann
tuned
2006-11-18, by haftmann
clarified module dependencies
2006-11-18, by haftmann
div is now a class
2006-11-18, by haftmann
reduced verbosity
2006-11-18, by haftmann
adjustments for class package
2006-11-18, by haftmann
added an intro lemma for freshness of products; set up
2006-11-17, by urbanc
more robust syntax for definition/abbreviation/notation;
2006-11-17, by wenzelm
'notation': more robust 'and' list;
2006-11-17, by wenzelm
updated;
2006-11-17, by wenzelm
added Isar.goal;
2006-11-17, by wenzelm
added where_;
2006-11-17, by wenzelm
add lemmas LIM_zero_iff, LIM_norm_zero_iff
2006-11-16, by huffman
Includes type:sort constraints in its code to collect predicates in axiom clauses.
2006-11-16, by paulson
Now includes only types used to instantiate overloaded constants in arity clauses
2006-11-16, by paulson
added General/basics.ML;
2006-11-16, by wenzelm
moved some fundamental concepts to General/basics.ML;
2006-11-16, by wenzelm
Fundamental concepts.
2006-11-16, by wenzelm
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
2006-11-15, by wenzelm
tuned proofs;
2006-11-15, by wenzelm
replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
2006-11-15, by wenzelm
replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
2006-11-15, by wenzelm
dropping accidental self-imports
2006-11-15, by haftmann
corrected polymorphism check
2006-11-15, by haftmann
clarified code for building function equation system; explicit check of type discipline
2006-11-15, by haftmann
moved evaluation to Code_Generator.thy
2006-11-15, by haftmann
added filter_set; adaptions to more strict type discipline for code lemmas
2006-11-15, by haftmann
moved transitivity rules to Orderings.thy
2006-11-15, by haftmann
added transitivity rules, reworking of min/max lemmas
2006-11-15, by haftmann
dropped dependency on sets
2006-11-15, by haftmann
reworking of min/max lemmas
2006-11-15, by haftmann
added interpretation
2006-11-15, by haftmann
removed HOL_css
2006-11-15, by haftmann
added evaluation oracle
2006-11-15, by haftmann
replaced exists_fresh lemma with a version formulated with obtains;
2006-11-15, by urbanc
updated;
2006-11-15, by wenzelm
Auxiliary antiquotations for Isabelle manuals.
2006-11-15, by wenzelm
common antiquote_setup.ML;
2006-11-15, by wenzelm
Arity clauses are now produced only for types and type classes actually used.
2006-11-15, by paulson
converted to 'inductive2';
2006-11-14, by wenzelm
added for_simple_fixes, specification;
2006-11-14, by wenzelm
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
2006-11-14, by wenzelm
removed fix_frees interface;
2006-11-14, by wenzelm
converted to 'inductive2';
2006-11-14, by wenzelm
inductive: canonical specification syntax (flattened result only);
2006-11-14, by wenzelm
inductive2: canonical specification syntax;
2006-11-14, by wenzelm
InductivePackage.add_inductive_i: canonical argument order;
2006-11-14, by wenzelm
inductive2: canonical specification syntax;
2006-11-14, by wenzelm
Exported some names
2006-11-14, by schirmer
simplified Proof.theorem(_i) interface -- removed target support;
2006-11-14, by wenzelm
simplified Proof.theorem(_i) interface;
2006-11-14, by wenzelm
antiquotation theory: plain Theory.requires, no peeking at ThyInfo;
2006-11-14, by wenzelm
simplified Proof.theorem(_i) interface;
2006-11-14, by wenzelm
tuned antiquotation theory;
2006-11-14, by wenzelm
value restriction
2006-11-14, by haftmann
removed old cygwin wrappers;
2006-11-14, by wenzelm
declare_constraints: reset constraint on dummyS;
2006-11-14, by wenzelm
removed Isar/isar_thy.ML;
2006-11-14, by wenzelm
added dummyS;
2006-11-14, by wenzelm
removed legacy read/cert/string_of;
2006-11-14, by wenzelm
recdef_tc(_i): local_theory interface via Specification.theorem_i;
2006-11-14, by wenzelm
incorporated IsarThy into IsarCmd;
2006-11-14, by wenzelm
removed theorem(_i);
2006-11-14, by wenzelm
upd
2006-11-13, by haftmann
atbroy51 broke down, switch to atbroy9
2006-11-13, by kleing
updated
2006-11-13, by krauss
antiquotation "theory": proper output, only check via ThyInfo.theory;
2006-11-13, by wenzelm
tuned;
2006-11-13, by wenzelm
added antiquotation @{theory name};
2006-11-13, by wenzelm
fixed comment -- oops;
2006-11-13, by wenzelm
adjusted to new fun''
2006-11-13, by haftmann
*** empty log message ***
2006-11-13, by haftmann
added antiquotation theory
2006-11-13, by haftmann
cleaned up
2006-11-13, by haftmann
added theory antiquotation
2006-11-13, by haftmann
combinator for overwriting changes with warning
2006-11-13, by haftmann
added higher-order combinators for structured results
2006-11-13, by haftmann
adjusted name in generated code
2006-11-13, by haftmann
dropped LOrder dependency
2006-11-13, by haftmann
moved upwars in HOL theory graph
2006-11-13, by haftmann
added thy dependencies
2006-11-13, by haftmann
PreList = Main - List
2006-11-13, by haftmann
introduces preorders
2006-11-13, by haftmann
dropped Inductive dependency
2006-11-13, by haftmann
dropped Typedef dependency
2006-11-13, by haftmann
added LOrder dependency
2006-11-13, by haftmann
tuned ml antiquotations
2006-11-13, by haftmann
adjusted
2006-11-13, by haftmann
tuned
2006-11-13, by haftmann
added tt tag
2006-11-13, by haftmann
auto_term => lexicographic_order
2006-11-13, by krauss
updated
2006-11-13, by krauss
replaced "auto_term" by the simpler method "relation", which does not try
2006-11-13, by krauss
added fresh_prodD, which is included fresh_prodD into mksimps setup;
2006-11-13, by wenzelm
added lexicographic_order.ML to makefile
2006-11-13, by krauss
image_constant_conv no longer [simp]
2006-11-12, by nipkow
instantiate: tuned indentity case;
2006-11-12, by wenzelm
removed dead code;
2006-11-12, by wenzelm
mk_atomize: careful matching against rules admits overloading;
2006-11-12, by wenzelm
started reorgnization of lattice theories
2006-11-12, by nipkow
Added in is_fol_thms.
2006-11-11, by mengj
level: do not account for local theory blocks (relevant for document preparation);
2006-11-11, by wenzelm
local 'end': no default tags;
2006-11-11, by wenzelm
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
2006-11-11, by wenzelm
removed obsolete context;
2006-11-11, by wenzelm
turned 'context' into plain thy_decl, discontinued thy_switch;
2006-11-11, by wenzelm
tuned proofs;
2006-11-11, by wenzelm
updated local theory targets;
2006-11-11, by wenzelm
updated local theory targets;
2006-11-11, by wenzelm
updated;
2006-11-11, by wenzelm
Update standard keyword files.
2006-11-11, by wenzelm
tuned comments;
2006-11-10, by wenzelm
tuned comments;
2006-11-10, by wenzelm
tuned names of start_timing,/end_timing/check_timer;
2006-11-10, by wenzelm
removed obsolete ML compatibility fragments;
2006-11-10, by wenzelm
avoid strange typing problem in MosML;
2006-11-10, by wenzelm
tuned names of start_timing,/end_timing/check_timer;
2006-11-10, by wenzelm
simplified local theory wrappers;
2006-11-10, by wenzelm
removed mapping;
2006-11-10, by wenzelm
simplified exit;
2006-11-10, by wenzelm
simplified LocalTheory.exit;
2006-11-10, by wenzelm
Improvement to classrel clauses: now outputs the minimum needed.
2006-11-10, by paulson
deleted all uses of sign_of as it's now the identity function
2006-11-10, by urbanc
tuned;
2006-11-10, by wenzelm
tuned Variable.trade;
2006-11-10, by wenzelm
introduces canonical AList functions for loop_tacs
2006-11-10, by haftmann
minor refinements
2006-11-10, by haftmann
redundancy checkes includes eta-expansion
2006-11-10, by haftmann
improved syntax
2006-11-10, by haftmann
added bounded_linear and bounded_bilinear locales
2006-11-10, by huffman
no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);
2006-11-10, by wenzelm
tuned comments;
2006-11-10, by wenzelm
added x86-cygwin;
2006-11-09, by wenzelm
oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.
2006-11-09, by chaieb
LocalTheory.restore;
2006-11-09, by wenzelm
init: '-' refers to global context;
2006-11-09, by wenzelm
abbrevs: return result;
2006-11-09, by wenzelm
Stack.map_top;
2006-11-09, by wenzelm
abbrevs: return result;
2006-11-09, by wenzelm
separate map_top/all;
2006-11-09, by wenzelm
abbrevs: return result (use LocalTheory.abbrevs directly);
2006-11-09, by wenzelm
tuned;
2006-11-09, by wenzelm
abbrevs: return result;
2006-11-09, by wenzelm
timing/tracing code removed
2006-11-09, by webertj
interpreters for fst and snd added
2006-11-09, by webertj
new CCS-based implementation that should work with PolyML 5.0
2006-11-09, by webertj
HOL: less/less_eq on bool, modified syntax;
2006-11-09, by wenzelm
removed obsolete locale_results;
2006-11-09, by wenzelm
tuned;
2006-11-09, by wenzelm
imports Binimial;
2006-11-09, by wenzelm
updated;
2006-11-09, by wenzelm
lfp_induct_set;
2006-11-09, by wenzelm
modified less/less_eq syntax to avoid "x < y < z" etc.;
2006-11-09, by wenzelm
added lemma mult_mono'
2006-11-09, by huffman
added LIM_norm and related lemmas
2006-11-09, by huffman
moved theories Parity, GCD, Binomial to Library;
2006-11-08, by wenzelm
added profiling code, improved handling of proof terms, generation of domain
2006-11-08, by krauss
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-11-08, by wenzelm
case_tr': proper handling of authentic consts;
2006-11-08, by wenzelm
removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);
2006-11-08, by wenzelm
renamed DatatypeHooks.invoke to all
2006-11-08, by haftmann
moved lemma eq_neq_eq_imp_neq to HOL
2006-11-08, by haftmann
renamed Lattice_Locales to Lattices
2006-11-08, by haftmann
abstract ordering theories
2006-11-08, by haftmann
obsolete (cf. ROOT.ML);
2006-11-08, by wenzelm
added structure Main (from Main.ML);
2006-11-08, by wenzelm
proper definition of add_zero_left/right;
2006-11-08, by wenzelm
removed NatArith.thy, Main.ML;
2006-11-08, by wenzelm
removed theory NatArith (now part of Nat);
2006-11-08, by wenzelm
* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".
2006-11-08, by wenzelm
moved contribution note to CONTRIBUTORS;
2006-11-08, by wenzelm
Made "termination by lexicographic_order" the default for "fun" definitions.
2006-11-08, by krauss
LIM_compose -> isCont_LIM_compose;
2006-11-08, by huffman
generalized types of of_nat and of_int to work with non-commutative types
2006-11-08, by huffman
untabified
2006-11-07, by krauss
complex goal statements: misc cleanup;
2006-11-07, by wenzelm
Added datatype hook to declare all case_congs as "fundef_cong" automatically.
2006-11-07, by krauss
removed obsolete theorem statements (cf. specification.ML);
2006-11-07, by wenzelm
tuned specifications;
2006-11-07, by wenzelm
fixed locale fact references;
2006-11-07, by wenzelm
removed obsolete print_state_hook;
2006-11-07, by wenzelm
theorem statements: incorporate Obtain.statement, tuned;
2006-11-07, by wenzelm
moved statement to specification.ML;
2006-11-07, by wenzelm
removed obsolete Locale.smart_theorem;
2006-11-07, by wenzelm