2011-05-05 blanchet removed unsound hAPP optimization
2011-05-04 blanchet versions of ! and ? for the ASCII-challenged Mirabelle
2011-05-04 blanchet smoother handling of ! and ? in type system names
2011-05-04 blanchet tuning
2011-05-04 blanchet compile + added monotonicity tests
2011-05-04 blanchet documentation tuning
2011-05-04 blanchet renamed "many_typed" to "simple" (as in simple types)
2011-05-04 blanchet update type system documentation
2011-05-04 blanchet added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
2011-05-04 blanchet document monotonic type systems
2011-05-04 blanchet exploit inferred monotonicity
2011-05-04 blanchet [mq]: nitpick_tuning
2011-05-04 blanchet fixed cardinality computation for function types such as "'a -> unit"
2011-05-04 blanchet monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
2011-05-04 wenzelm proper case_names for int_cases, int_of_nat_induct;
2011-05-04 blanchet added type annotation for SML/NJ
2011-05-04 blanchet eta-expansion for SML/NJ
2011-05-03 wenzelm removed odd historical material;
2011-05-03 wenzelm merged
2011-05-03 blanchet fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
2011-05-03 blanchet cosmetics
2011-05-03 wenzelm more conventional naming scheme: names_long, names_short, names_unique;
2011-05-03 wenzelm railsetup required for IsarRef/style;
2011-05-03 wenzelm fit page;
2011-05-03 wenzelm use existing \<hyphen>;
2011-05-03 wenzelm more precise syntax diagram;
2011-05-03 wenzelm simplified rail configuration;
2011-05-03 wenzelm provide \isabellestyle{itunderscore} (requires underscore.sty);
2011-05-03 wenzelm updated generated files;
2011-05-03 wenzelm proper treatment of empty name -- avoid excessive vertical space;
2011-05-03 wenzelm final \makeatother -- catcodes appear to be global;
2011-05-03 blanchet fixed long name truncation logic
2011-05-03 wenzelm some documentation of @{rail} antiquotation;
2011-05-03 wenzelm more precise source position for @{rail};
2011-05-03 wenzelm sane paragraph layout;
2011-05-03 wenzelm updated configuration options -- no ML here;
2011-05-03 wenzelm tag ML as in IsarImplementation;
2011-05-03 wenzelm treat underscore as in IsarRef;
2011-05-03 wenzelm reactivated codegen example based on Lambda.thy;
2011-05-03 wenzelm formal Base theory;
2011-05-03 blanchet reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
2011-05-03 blanchet whitespace tuning
2011-05-03 blanchet make SML/NJ happiest
2011-05-02 blanchet no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
2011-05-02 blanchet replaced some Unsynchronized.refs with Config.Ts
2011-05-02 blanchet do not declare TPTP built-ins, e.g. $true
2011-05-02 blanchet SNARK workaround
2011-05-02 blanchet better default type systems for SNARK and ToFoF
2011-05-02 blanchet tuning
2011-05-02 blanchet recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
2011-05-02 blanchet generate tags for simps, intros, and elims in TPTP poblems on demand
2011-05-02 blanchet proper default for TPTP source filed
2011-05-02 blanchet have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-02 wenzelm eliminated old CVS Ids;
2011-05-02 wenzelm no use of package rail;
2011-05-02 wenzelm obsolete;
(0) -30000 -10000 -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip