isa-incredible.git
2016-05-20 Joachim BreitnerUse Eisbach’s solves in apply scripts master AFP-Submission
2016-05-20 Denis Lohneradd Stream_Ext to document
2016-05-20 Denis Lohnerfix import of Stream
2016-05-20 Denis Lohnerremove subsubsection Task 1.1 in Predicate_Tasks
2016-05-20 Denis Lohnerrefactor duplicate fact sset_cycle
2016-05-20 Joachim BreitnerInclude Predicate Task in document
2016-05-19 Joachim BreitnerRepair proof (simpler now)
2016-05-19 Joachim BreitnerFinish acyclicity
2016-05-19 Joachim BreitnerOne sorry left
2016-05-19 Joachim BreitnerPrunedness
2016-05-19 Joachim BreitnerSmall steps
2016-05-19 Joachim BreitnerMultiple interpretation commands make it easier
2016-05-19 Joachim BreitnerExample tasks using predicate (unfinished)
2016-05-19 Joachim BreitnerIncredible_Propositional should not depend on Natural_D...
2016-05-19 Joachim BreitnerAdd Incredible_Predicate.thy
2016-05-19 Joachim BreitnerAdd Predicate Formula instantiation
2016-05-19 Denis Lohnercomment and refactor propositional
2016-05-19 Denis Lohnerwording and parantheses
2016-05-19 Denis LohnerUse HOL instead of HOLCF in session
2016-05-19 Denis Lohneradd Task 2.11
2016-05-19 Denis LohnerPropositional: rename Const -> Fun and C -> Const
2016-05-19 Denis Lohnerprettify sset_cycle
2016-05-19 Denis Lohnerrename facts to avoid 'Duplicate fact declaration'...
2016-05-19 Denis LohnerNode -> RNode
2016-05-19 Denis Lohnerproof of sset_cycle
2016-05-19 Joachim BreitnerFinish instantiation, and split theory into multiple
2016-05-19 Denis LohnerStart of interpretation for propositional logic
2016-05-19 Joachim BreitnerTitelei
2016-05-19 Joachim BreitnerPresentation polish
2016-05-19 Joachim BreitnerPut rose_trees in a separate file
2016-05-19 Joachim BreitnerFactor out a general rose tree data type
2016-05-19 Joachim BreitnerLess case_tac
2016-05-19 Joachim BreitnerAll hail inductive_cases
2016-05-18 Joachim BreitnerMove some prefix-related lemmas
2016-05-18 Joachim BreitnerSplit out Inits theory
2016-05-18 Joachim BreitnerDocument setup
2016-05-18 Joachim BreitnerUn-Sorry
2016-05-18 Denis Lohnerreintroduce a sorry
2016-05-18 Denis Lohnerremove parameter fresh_vars
2016-05-18 Joachim BreitnerLemma moved
2016-05-18 Joachim BreitnerAll sories gone!
2016-05-18 Joachim BreitnerIncredible_Completeness only needs plain_iwf
2016-05-18 Joachim BreitnerFix local_iwf_it
2016-05-18 Joachim BreitnerComplete sublocale Well_Scoped_Instantiation
2016-05-18 Joachim BreitnerGet rid of a few sorries
2016-05-18 Joachim Breitnerrerename needs an explicit set
2016-05-18 Joachim Breitnertowards rerename_subst
2016-05-18 Joachim BreitnerImplement rerename
2016-05-18 Denis Lohneradd missing 'end'
2016-05-17 Joachim BreitnerKleine Schritte
2016-05-17 Joachim BreitnerInjectivity of labels is given
2016-05-17 Joachim BreitnerTowards variable globalization
2016-05-17 Joachim BreitnerSplit off Build_Incredible_Tree
2016-05-17 Joachim BreitnerUse list in trees, nat list as paths
2016-05-17 Joachim BreitnerAdd subst_renameLCs
2016-05-17 Joachim BreitnerAbstractFormulas: Talk about local constants
2016-05-13 Joachim BreitnerCompleteness: Use annotations instead of fidx
2016-05-12 Joachim Breitners/oops/qed/
2016-05-12 Joachim BreitnerIntroduce vidx
2016-05-12 Joachim BreitnerMerge 'preform and 'form
2016-05-12 Denis Lohnerintroduce polymorphic annotations
2016-05-12 Denis Lohnerfix assumption conclusions_closed
2016-05-12 Joachim BreitnerTowards scoped variables
2016-05-11 Joachim BreitnerTighten well_scoped_inst
2016-05-11 Joachim BreitnerFactor out fidx_iAnnot (unproven)
2016-05-11 Joachim BreitnerTry to get tree stuff into a file of its own
2016-05-10 Joachim Breitnerto_form_conc_forms
2016-02-26 Joachim BreitnerShow that edge labels match up
2016-02-25 Joachim BreitnerDefine hyp edges
2016-02-23 Joachim BreitnerOn the existence of hypothesis along the way
2016-02-23 Joachim BreitnerIntroduce HNode
2016-02-23 Joachim BreitnerCleanup, prunedness
2016-02-23 Joachim BreitnerNight shift: categorize scope via prefix
2016-02-22 Joachim BreitnerMore on completeness, but it feels like the wrong way...
2016-02-22 Joachim BreitnerCheckpoint completeness proof
2016-02-22 Joachim BreitnerIsabelle2016 compat
2016-02-21 Joachim BreitnerAdd forgotten files
2016-02-21 Joachim BreitnerA somewhat elaborated tree
2016-02-21 Joachim BreitnerAdd Helper blocks, and Cuts
2016-02-21 Joachim Breitnerstuff towards completeness
2016-02-12 Joachim BreitnerIntroduce an elaborated tree
2016-02-12 Joachim BreitnerIntroduce the notion of a terminal path
2016-02-11 Joachim BreitnerRelax requirement on fv (subst s v)
2016-02-04 Joachim BreitnerCorrectness, now also for predicate logics
2016-02-04 Joachim Breitners/annotate/freshen/g
2016-02-04 Joachim BreitnerNicer definition of eff
2016-02-04 Joachim BreitnerStructured type for the antecedent
2016-02-03 Joachim BreitnerFirst attempt at specifying fresh variables
2016-02-03 Joachim BreitnerFiniteness
2016-02-02 Joachim BreitnerAdd gitignore
2016-02-02 Joachim BreitnerNotion of "solved"
2016-02-02 Joachim BreitnerSimplify
2016-02-02 Joachim BreitnerBeginning of an Isabelle Formalisation