allowing indentation of 'theory' keyword

simplified after_qed;

avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;

removed export_plain; (some_)fact_tac: Drule.incr_indexes;

renamed assert_prop to ensure_prop;

renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;

export compose_hhf; removed obsolete norm_hhf_plain; tuned;

removed impose_hyps, satisfy_hyps; tuned;

const args: do not store variable names (unused);

renamed goals.ML to old_goals.ML;

(fix for accidental commit)

(codegen)

generate pattern combinators for new datatypes

reimplemented Case syntax using print/parse translations; moved as-patterns to separate section

add case syntax for type one

remove syntax for as-patterns

avoid 'as' as identifier;

avoid 'as' as identifier;

Added strong induction theorem (currently only axiomatized!).

Initial commit.

Initial commit of the theory "Weakening".

added thms perm, distinct and fresh to the simplifier. One would liket to add also inject, but this causes problems with "congruences" like Lam [a].t1 = Lam [b].t2 P (Lam [a].t1) ----------------------- P (Lam [b].t2) because the equation "Lam [a].t1 = Lam [b].t2" would simplify to "[a].t1 = [b].t2" and then the goal is not true just by simplification.

added proper fillin_mixfix

added fillin_mixfix, replace_quote

New function store_thmss_atts.

used the function Library.product for the cprod from Stefan

fixed bug with nominal induct - the bug occured in rule inductions when the goal did not use all variables from the relation over which the induction was done

added fillin_mixfix' needed by serializer

add case syntax stuff

use consts for infix syntax

add proof of Bekic's theorem: fix_cprod

simplify definitions

put iterate and fix in separate sections; added Letrec

renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM

add line breaks to Rep_CFun syntax

moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section

moved adm_chfindom from Fix.thy to Cfun.thy

cleaned up

add print translation: Abs_CFun f => LAM x. f x

Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names. Also removed some functions that are not used any more.

improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion

reimplement copy_def to use data constructor constants

cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple

generate lambda pattern syntax for new data constructors

changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF

add constant one_when; LAM pattern for ONE

add translation for wildcard pattern

change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up

make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1

cleaned up; ch2ch_Rep_CFun is a simp rule

changed iterate to a continuous type

reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less

removed ex/loeckx.ML

removed proof about Ifix, which no longer exists

cleaned up; chain_const and thelub_const are simp rules

cleaned up; removed adm_tricks in favor of compactness theorems