lib/Tools/update_theorems
changeset 61337 4645502c3c64
child 62450 2154f709fc25
equal deleted inserted replaced
61336:fa4ebbd350ae 61337:4645502c3c64
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Author: Makarius
       
     4 #
       
     5 # DESCRIPTION: update toplevel theorem keywords
       
     6 
       
     7 
       
     8 ## diagnostics
       
     9 
       
    10 PRG="$(basename "$0")"
       
    11 
       
    12 function usage()
       
    13 {
       
    14   echo
       
    15   echo "Usage: isabelle $PRG [FILES|DIRS...]"
       
    16   echo
       
    17   echo "  Recursively find .thy files and update toplevel theorem keywords:"
       
    18   echo
       
    19   echo "    theorems             ~>  lemmas"
       
    20   echo "    schematic_theorem    ~>  schematic_goal"
       
    21   echo "    schematic_lemma      ~>  schematic_goal"
       
    22   echo "    schematic_corollary  ~>  schematic_goal"
       
    23   echo
       
    24   echo "  Old versions of files are preserved by appending \"~~\"."
       
    25   echo
       
    26   exit 1
       
    27 }
       
    28 
       
    29 
       
    30 ## process command line
       
    31 
       
    32 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
       
    33 
       
    34 SPECS="$@"; shift "$#"
       
    35 
       
    36 
       
    37 ## main
       
    38 
       
    39 find $SPECS -name \*.thy -print0 | \
       
    40   xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Theorems