expanded tabs
authorclasohm
Mon Feb 05 13:44:28 1996 +0100 (1996-02-05)
changeset 1473e8d4606e6502
parent 1472 a89803e3d1bd
child 1474 3f7d67927fe2
expanded tabs
src/FOL/ex/List.thy
src/FOL/ex/Nat.thy
src/FOL/ex/Nat2.thy
src/FOL/ex/Prolog.thy
src/FOL/ex/foundn.ML
     1.1 --- a/src/FOL/ex/List.thy	Fri Feb 02 12:05:24 1996 +0100
     1.2 +++ b/src/FOL/ex/List.thy	Mon Feb 05 13:44:28 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	FOL/ex/list
     1.5 +(*  Title:      FOL/ex/list
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow
     1.8 +    Author:     Tobias Nipkow
     1.9      Copyright   1991  University of Cambridge
    1.10  
    1.11  Examples of simplification and induction on lists
    1.12 @@ -12,14 +12,14 @@
    1.13  arities list :: (term)term
    1.14  
    1.15  consts
    1.16 -   hd		:: 'a list => 'a  
    1.17 -   tl		:: 'a list => 'a list
    1.18 -   forall	:: ['a list, 'a => o] => o  
    1.19 -   len		:: 'a list => nat  
    1.20 -   at		:: ['a list, nat] => 'a  
    1.21 -   "[]"		:: ('a list)  	                     ("[]")
    1.22 -   "."		:: ['a, 'a list] => 'a list          (infixr 80)
    1.23 -   "++"		:: ['a list, 'a list] => 'a list     (infixr 70)
    1.24 +   hd           :: 'a list => 'a  
    1.25 +   tl           :: 'a list => 'a list
    1.26 +   forall       :: ['a list, 'a => o] => o  
    1.27 +   len          :: 'a list => nat  
    1.28 +   at           :: ['a list, nat] => 'a  
    1.29 +   "[]"         :: ('a list)                         ("[]")
    1.30 +   "."          :: ['a, 'a list] => 'a list          (infixr 80)
    1.31 +   "++"         :: ['a list, 'a list] => 'a list     (infixr 70)
    1.32  
    1.33  rules
    1.34   list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"
    1.35 @@ -30,12 +30,12 @@
    1.36   list_distinct1 "~[] = x.l"
    1.37   list_distinct2 "~x.l = []"
    1.38  
    1.39 - list_free 	"x.l = x'.l' <-> x=x' & l=l'"
    1.40 + list_free      "x.l = x'.l' <-> x=x' & l=l'"
    1.41  
    1.42 - app_nil 	"[]++l = l"
    1.43 - app_cons 	"(x.l)++l' = x.(l++l')"
    1.44 - tl_eq 	"tl(m.q) = q"
    1.45 - hd_eq 	"hd(m.q) = m"
    1.46 + app_nil        "[]++l = l"
    1.47 + app_cons       "(x.l)++l' = x.(l++l')"
    1.48 + tl_eq  "tl(m.q) = q"
    1.49 + hd_eq  "hd(m.q) = m"
    1.50  
    1.51   forall_nil "forall([],P)"
    1.52   forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
     2.1 --- a/src/FOL/ex/Nat.thy	Fri Feb 02 12:05:24 1996 +0100
     2.2 +++ b/src/FOL/ex/Nat.thy	Mon Feb 05 13:44:28 1996 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4 -(*  Title: 	FOL/ex/nat.thy
     2.5 +(*  Title:      FOL/ex/nat.thy
     2.6      ID:         $Id$
     2.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.9      Copyright   1992  University of Cambridge
    2.10  
    2.11  Examples for the manual "Introduction to Isabelle"
     3.1 --- a/src/FOL/ex/Nat2.thy	Fri Feb 02 12:05:24 1996 +0100
     3.2 +++ b/src/FOL/ex/Nat2.thy	Mon Feb 05 13:44:28 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	FOL/ex/nat2.thy
     3.5 +(*  Title:      FOL/ex/nat2.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Tobias Nipkow
     3.8 +    Author:     Tobias Nipkow
     3.9      Copyright   1994  University of Cambridge
    3.10  
    3.11  Theory for examples of simplification and induction on the natural numbers
    3.12 @@ -13,28 +13,28 @@
    3.13  
    3.14  consts
    3.15   succ,pred :: nat => nat  
    3.16 -       "0" :: nat  	("0")
    3.17 +       "0" :: nat       ("0")
    3.18         "+" :: [nat,nat] => nat   (infixr 90)
    3.19    "<","<=" :: [nat,nat] => o     (infixr 70)
    3.20  
    3.21  rules
    3.22 - pred_0		"pred(0) = 0"
    3.23 - pred_succ	"pred(succ(m)) = m"
    3.24 + pred_0         "pred(0) = 0"
    3.25 + pred_succ      "pred(succ(m)) = m"
    3.26  
    3.27 - plus_0		"0+n = n"
    3.28 - plus_succ	"succ(m)+n = succ(m+n)"
    3.29 + plus_0         "0+n = n"
    3.30 + plus_succ      "succ(m)+n = succ(m+n)"
    3.31  
    3.32 - nat_distinct1	"~ 0=succ(n)"
    3.33 - nat_distinct2	"~ succ(m)=0"
    3.34 - succ_inject	"succ(m)=succ(n) <-> m=n"
    3.35 + nat_distinct1  "~ 0=succ(n)"
    3.36 + nat_distinct2  "~ succ(m)=0"
    3.37 + succ_inject    "succ(m)=succ(n) <-> m=n"
    3.38  
    3.39 - leq_0		"0 <= n"
    3.40 - leq_succ_succ	"succ(m)<=succ(n) <-> m<=n"
    3.41 - leq_succ_0	"~ succ(m) <= 0"
    3.42 + leq_0          "0 <= n"
    3.43 + leq_succ_succ  "succ(m)<=succ(n) <-> m<=n"
    3.44 + leq_succ_0     "~ succ(m) <= 0"
    3.45  
    3.46 - lt_0_succ	"0 < succ(n)"
    3.47 - lt_succ_succ	"succ(m)<succ(n) <-> m<n"
    3.48 + lt_0_succ      "0 < succ(n)"
    3.49 + lt_succ_succ   "succ(m)<succ(n) <-> m<n"
    3.50   lt_0 "~ m < 0"
    3.51  
    3.52 - nat_ind	"[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
    3.53 + nat_ind        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
    3.54  end
     4.1 --- a/src/FOL/ex/Prolog.thy	Fri Feb 02 12:05:24 1996 +0100
     4.2 +++ b/src/FOL/ex/Prolog.thy	Mon Feb 05 13:44:28 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	FOL/ex/prolog.thy
     4.5 +(*  Title:      FOL/ex/prolog.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.9      Copyright   1992  University of Cambridge
    4.10  
    4.11  First-Order Logic: PROLOG examples
     5.1 --- a/src/FOL/ex/foundn.ML	Fri Feb 02 12:05:24 1996 +0100
     5.2 +++ b/src/FOL/ex/foundn.ML	Mon Feb 05 13:44:28 1996 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      FOL/ex/foundn
     5.5 +(*  Title:      FOL/ex/foundn.ML
     5.6      ID:         $Id$
     5.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8      Copyright   1991  University of Cambridge
     5.9 @@ -6,7 +6,7 @@
    5.10  Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
    5.11  *)
    5.12  
    5.13 -writeln"File FOL/ex/foundn.";
    5.14 +writeln"File FOL/ex/foundn.ML";
    5.15  
    5.16  goal IFOL.thy "A&B  --> (C-->A&C)";
    5.17  by (rtac impI 1);