src/Pure/Isar/isar_syn.ML
changeset 5914 2c069b0a98ee
parent 5896 4a75d89e2818
child 5924 b9d5f5901b59
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 17 14:12:13 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 17 14:13:32 1998 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4    - 'result' command;
     1.5    - '--' (comment) option everywhere;
     1.6    - 'chapter', 'section' etc.;
     1.7 +  - 'thm': xthms1;
     1.8  *)
     1.9  
    1.10  signature ISAR_SYN =
    1.11 @@ -131,8 +132,8 @@
    1.12  
    1.13  (* axioms and definitions *)
    1.14  
    1.15 -val spec = thm_name -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.16 -val spec' = opt_thm_name -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.17 +val spec = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.18 +val spec' = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.19  
    1.20  val axiomsP =
    1.21    OuterSyntax.parser false "axioms" "state arbitrary propositions (axiomatic!)"
    1.22 @@ -143,6 +144,19 @@
    1.23      (Scan.repeat1 spec' >> (Toplevel.theory o IsarThy.add_defs));
    1.24  
    1.25  
    1.26 +(* theorems *)
    1.27 +
    1.28 +val facts = opt_thm_name "=" -- xthms1;
    1.29 +
    1.30 +val theoremsP =
    1.31 +  OuterSyntax.parser false "theorems" "define theorems"
    1.32 +    (facts >> (Toplevel.theory o IsarThy.have_theorems));
    1.33 +
    1.34 +val lemmasP =
    1.35 +  OuterSyntax.parser false "lemmas" "define lemmas"
    1.36 +    (facts >> (Toplevel.theory o IsarThy.have_lemmas));
    1.37 +
    1.38 +
    1.39  (* axclass *)
    1.40  
    1.41  val axclassP =
    1.42 @@ -232,7 +246,7 @@
    1.43  
    1.44  (* statements *)
    1.45  
    1.46 -fun statement f = opt_thm_name -- prop >> (fn ((x, y), z) => f x y z);
    1.47 +fun statement f = opt_thm_name ":" -- prop >> (fn ((x, y), z) => f x y z);
    1.48  
    1.49  val theoremP =
    1.50    OuterSyntax.parser false "theorem" "state theorem"
    1.51 @@ -251,27 +265,31 @@
    1.52      (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
    1.53  
    1.54  
    1.55 -(* forward chaining *)
    1.56 +(* facts *)
    1.57  
    1.58  val thenP =
    1.59    OuterSyntax.parser false "then" "forward chaining"
    1.60      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
    1.61  
    1.62  val fromP =
    1.63 -  OuterSyntax.parser false "from" "forward chaining, from given facts"
    1.64 -    (enum1 "," xname >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
    1.65 +  OuterSyntax.parser false "from" "forward chaining from given facts"
    1.66 +    (xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
    1.67 +
    1.68 +val factsP =
    1.69 +  OuterSyntax.parser false "note" "define facts"
    1.70 +    (facts >> (Toplevel.proof o IsarThy.have_facts));
    1.71  
    1.72  
    1.73  (* proof context *)
    1.74  
    1.75  val assumeP =
    1.76    OuterSyntax.parser false "assume" "assume propositions"
    1.77 -    (opt_thm_name -- enum1 "," prop >>
    1.78 +    (opt_thm_name ":" -- Scan.repeat1 prop >>
    1.79        (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
    1.80  
    1.81  val fixP =
    1.82    OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
    1.83 -    (enum1 "," (name -- Scan.option ($$$ "::" |-- typ))
    1.84 +    (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
    1.85        >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
    1.86  
    1.87  val letP =
    1.88 @@ -398,12 +416,7 @@
    1.89      (Scan.succeed IsarCmd.print_lthms);
    1.90  
    1.91  val print_thmsP =
    1.92 -  OuterSyntax.parser true "thms" "print theorems"
    1.93 -    (xname -- opt_attribs >> IsarCmd.print_thms);
    1.94 -
    1.95 -val print_thmP =
    1.96 -  OuterSyntax.parser true "thm" "print theorem"
    1.97 -    (xname -- opt_attribs >> IsarCmd.print_thm);
    1.98 +  OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms);
    1.99  
   1.100  val print_propP =
   1.101    OuterSyntax.parser true "print_prop" "read and print proposition"
   1.102 @@ -457,7 +470,7 @@
   1.103      (Scan.succeed IsarCmd.exit);
   1.104  
   1.105  val breakP =
   1.106 -  OuterSyntax.parser true "break" "discontinue execution"
   1.107 +  OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
   1.108      (Scan.succeed IsarCmd.break);
   1.109  
   1.110  
   1.111 @@ -478,19 +491,19 @@
   1.112    (*theory sections*)
   1.113    textP, classesP, classrelP, defaultsortP, typedeclP, typeabbrP,
   1.114    nontermP, aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   1.115 -  axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,
   1.116 -  parse_ast_translationP, parse_translationP, print_translationP,
   1.117 -  typed_print_translationP, print_ast_translationP,
   1.118 -  token_translationP, oracleP,
   1.119 +  theoremsP, lemmasP, axclassP, instanceP, globalP, localP, pathP,
   1.120 +  useP, mlP, setupP, parse_ast_translationP, parse_translationP,
   1.121 +  print_translationP, typed_print_translationP,
   1.122 +  print_ast_translationP, token_translationP, oracleP,
   1.123    (*proof commands*)
   1.124    theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
   1.125 -  beginP, nextP, qedP, qed_withP, kill_proofP, refineP, then_refineP,
   1.126 -  proofP, terminal_proofP, trivial_proofP, default_proofP,
   1.127 -  clear_undoP, undoP, redoP, backP, prevP, upP, topP,
   1.128 +  factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
   1.129 +  then_refineP, proofP, terminal_proofP, trivial_proofP,
   1.130 +  default_proofP, clear_undoP, undoP, redoP, backP, prevP, upP, topP,
   1.131    (*diagnostic commands*)
   1.132    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   1.133    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   1.134 -  print_thmP, print_thmsP, print_propP, print_termP, print_typeP,
   1.135 +  print_thmsP, print_propP, print_termP, print_typeP,
   1.136    (*system commands*)
   1.137    cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
   1.138