Changeset 11602

Show
Ignore:
Timestamp:
26.03.2009 18:04:46 (12 months ago)
Author:
maeder
Message:

wibble

Location:
trunk/Proofs
Files:
3 modified

Legend:

Unmodified
Added
Removed

  • trunk/Proofs/InferBasic.hs

    r11596 r11602  
    276276                          freedefs 
    277277        ps <- lift $ proveTheory lid p (theoryName st) th freedefs1 
    278         -- lift $ putStrLn $ show ps 
    279278        let st' = markProved acm lid ps st 
    280279        lift $ addProveToHist intSt st' 

  • trunk/Proofs/Local.hs

    r11573 r11602  
    11{- | 
    22Module      :  $Header$ 
    3 Description :  local proof rukes for development graphs 
     3Description :  local proof rules for development graphs 
    44Copyright   :  (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006 
    55License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt 

  • trunk/Proofs/TheoremHideShift.hs

    r11601 r11602  
    116116  let localTh = dgn_theory nodelab in 
    117117  if isDGRef nodelab then do 
    118     let refLn = dgn_libname nodelab 
    119         refNode = dgn_node nodelab 
     118    let refNode = dgn_node nodelab 
    120119        dg' = lookupDGraph (dgn_libname nodelab) libEnv 
    121120        newLab = labDG dg' refNode