Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Typefix.thy
branchisac-update-Isa09-2
changeset 37948 ed85f172569c
parent 37947 22235e4dbe5f
child 37949 aaf528d3ebd5
equal deleted inserted replaced
37947:22235e4dbe5f 37948:ed85f172569c 
     1 (* Title:  fixed type for _RE_parsing of strings from frontend 
     1 (* Title:  fixed type for _RE_parsing of strings from frontend 
     2    Author: Walther Neuper
 
     2    Author: Walther Neuper, hints from Makarius Wenzel
 
     3    9911xx 
     3    9911xx 
     4    (c) due to copyright terms
 
     4    (c) due to copyright terms
 
     5    with hints from Markus Wenzel
 
       
     6  *)
 
     5  *)
 
     7 
     6 
     8 theory Typefix imports "../ProgLang/Script" begin
 
     7 theory Typefix imports "ProgLang/Script" begin
 
       
     8 (*theory Typefix imports "../ProgLang/Script" begin*)
 
     9 
     9 
    10 syntax
 
    10 syntax
 
    11        
    11        
    12   "_plus"  :: 'a
 
    12   "_plus"  :: 'a
 
    13   "_minus" :: 'a
 
    13   "_minus" :: 'a
wneuper/isa